Theorem zfpair

Description: The Axiom of Pairing of Zermelo-Fraenkel set theory. Axiom 2 of TakeutiZaring p. 15. In some textbooks this is stated as a separate axiom; here we show it is redundant since it can be derived from the other axioms.

This theorem should not be referenced by any proof other than axprALT . Instead, use zfpair2 below so that the uses of the Axiom of Pairing can be more easily identified. (Contributed by NM, 18-Oct-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	zfpair	|- { x , y } e. _V

Proof

Step	Hyp	Ref	Expression
1		dfpr2	|- { x , y } = { w | ( w = x \/ w = y ) }
2		19.43	|- ( E. z ( ( z = (/) /\ w = x ) \/ ( z = { (/) } /\ w = y ) ) <-> ( E. z ( z = (/) /\ w = x ) \/ E. z ( z = { (/) } /\ w = y ) ) )
3		prlem2	|- ( ( ( z = (/) /\ w = x ) \/ ( z = { (/) } /\ w = y ) ) <-> ( ( z = (/) \/ z = { (/) } ) /\ ( ( z = (/) /\ w = x ) \/ ( z = { (/) } /\ w = y ) ) ) )
4	3	exbii	|- ( E. z ( ( z = (/) /\ w = x ) \/ ( z = { (/) } /\ w = y ) ) <-> E. z ( ( z = (/) \/ z = { (/) } ) /\ ( ( z = (/) /\ w = x ) \/ ( z = { (/) } /\ w = y ) ) ) )
5		0ex	|- (/) e. _V
6	5	isseti	|- E. z z = (/)
7		19.41v	|- ( E. z ( z = (/) /\ w = x ) <-> ( E. z z = (/) /\ w = x ) )
8	6 7	mpbiran	|- ( E. z ( z = (/) /\ w = x ) <-> w = x )
9		p0ex	|- { (/) } e. _V
10	9	isseti	|- E. z z = { (/) }
11		19.41v	|- ( E. z ( z = { (/) } /\ w = y ) <-> ( E. z z = { (/) } /\ w = y ) )
12	10 11	mpbiran	|- ( E. z ( z = { (/) } /\ w = y ) <-> w = y )
13	8 12	orbi12i	|- ( ( E. z ( z = (/) /\ w = x ) \/ E. z ( z = { (/) } /\ w = y ) ) <-> ( w = x \/ w = y ) )
14	2 4 13	3bitr3ri	|- ( ( w = x \/ w = y ) <-> E. z ( ( z = (/) \/ z = { (/) } ) /\ ( ( z = (/) /\ w = x ) \/ ( z = { (/) } /\ w = y ) ) ) )
15	14	abbii	|- { w | ( w = x \/ w = y ) } = { w | E. z ( ( z = (/) \/ z = { (/) } ) /\ ( ( z = (/) /\ w = x ) \/ ( z = { (/) } /\ w = y ) ) ) }
16		dfpr2	|- { (/) , { (/) } } = { z | ( z = (/) \/ z = { (/) } ) }
17		pp0ex	|- { (/) , { (/) } } e. _V
18	16 17	eqeltrri	|- { z | ( z = (/) \/ z = { (/) } ) } e. _V
19		equequ2	|- ( v = x -> ( w = v <-> w = x ) )
20		0inp0	|- ( z = (/) -> -. z = { (/) } )
21	19 20	prlem1	|- ( v = x -> ( z = (/) -> ( ( ( z = (/) /\ w = x ) \/ ( z = { (/) } /\ w = y ) ) -> w = v ) ) )
22	21	alrimdv	|- ( v = x -> ( z = (/) -> A. w ( ( ( z = (/) /\ w = x ) \/ ( z = { (/) } /\ w = y ) ) -> w = v ) ) )
23	22	spimevw	|- ( z = (/) -> E. v A. w ( ( ( z = (/) /\ w = x ) \/ ( z = { (/) } /\ w = y ) ) -> w = v ) )
24		orcom	|- ( ( ( z = (/) /\ w = x ) \/ ( z = { (/) } /\ w = y ) ) <-> ( ( z = { (/) } /\ w = y ) \/ ( z = (/) /\ w = x ) ) )
25		equequ2	|- ( v = y -> ( w = v <-> w = y ) )
26	20	con2i	|- ( z = { (/) } -> -. z = (/) )
27	25 26	prlem1	|- ( v = y -> ( z = { (/) } -> ( ( ( z = { (/) } /\ w = y ) \/ ( z = (/) /\ w = x ) ) -> w = v ) ) )
28	24 27	syl7bi	|- ( v = y -> ( z = { (/) } -> ( ( ( z = (/) /\ w = x ) \/ ( z = { (/) } /\ w = y ) ) -> w = v ) ) )
29	28	alrimdv	|- ( v = y -> ( z = { (/) } -> A. w ( ( ( z = (/) /\ w = x ) \/ ( z = { (/) } /\ w = y ) ) -> w = v ) ) )
30	29	spimevw	|- ( z = { (/) } -> E. v A. w ( ( ( z = (/) /\ w = x ) \/ ( z = { (/) } /\ w = y ) ) -> w = v ) )
31	23 30	jaoi	|- ( ( z = (/) \/ z = { (/) } ) -> E. v A. w ( ( ( z = (/) /\ w = x ) \/ ( z = { (/) } /\ w = y ) ) -> w = v ) )
32	18 31	zfrep4	|- { w | E. z ( ( z = (/) \/ z = { (/) } ) /\ ( ( z = (/) /\ w = x ) \/ ( z = { (/) } /\ w = y ) ) ) } e. _V
33	15 32	eqeltri	|- { w | ( w = x \/ w = y ) } e. _V
34	1 33	eqeltri	|- { x , y } e. _V