sb56 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > sb56		Unicode version

Theorem sb56 2098

Description: Two equivalent ways of expressing the proper substitution of

for

, when

and

are distinct. Theorem 6.2 of [Quine] p. 40. The proof does not involve df-sb 1649. (Contributed by NM, 14-Apr-2008.)

**Assertion**
Ref	Expression
sb56	$/\$

(

)

**Proof of Theorem sb56**
Step	Hyp	Ref	Expression
1		nfa1 1788	. 2
2		ax11v 2096	. . 3
3		sp 1747	. . . 4
4	3	com12 27	. . 3
5	2, 4	impbid 183	. 2
6	1, 5	equsex 1962	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 176 $/\$ wa 358

wal 1540

wex 1541

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925

This theorem depends on definitions: df-bi 177 df-an 360 df-tru 1319 df-ex 1542 df-nf 1545

This theorem is referenced by: sb6 2099 sb5 2100 alexeq 2968