Theorem axpr

Description: Unabbreviated version of the Axiom of Pairing of ZF set theory, derived as a theorem from the other axioms.

This theorem should not be referenced by any proof. Instead, use ax-pr below so that the uses of the Axiom of Pairing can be more easily identified.

For a shorter proof using ax-ext , see axprALT . (Contributed by NM, 14-Nov-2006) Remove dependency on ax-ext . (Revised by Rohan Ridenour, 10-Aug-2023) (Proof shortened by BJ, 13-Aug-2023) (Proof shortened by Matthew House, 18-Sep-2025) Use ax-pr instead. (New usage is discouraged.)

	Ref	Expression
Assertion	axpr	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )

Proof

Step	Hyp	Ref	Expression
1		axprlem3	|- E. z A. w ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) )
2		axprlem1	|- E. s A. n ( A. t -. t e. n -> n e. s )
3	2	sepexi	|- E. s A. n ( n e. s <-> A. t -. t e. n )
4		biimp	|- ( ( n e. s <-> A. t -. t e. n ) -> ( n e. s -> A. t -. t e. n ) )
5		ax-nul	|- E. n A. t -. t e. n
6		exbi	|- ( A. n ( n e. s <-> A. t -. t e. n ) -> ( E. n n e. s <-> E. n A. t -. t e. n ) )
7	5 6	mpbiri	|- ( A. n ( n e. s <-> A. t -. t e. n ) -> E. n n e. s )
8		ifptru	|- ( E. n n e. s -> ( if- ( E. n n e. s , w = x , w = y ) <-> w = x ) )
9	7 8	syl	|- ( A. n ( n e. s <-> A. t -. t e. n ) -> ( if- ( E. n n e. s , w = x , w = y ) <-> w = x ) )
10	3 4 9	axprlem4	|- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( w = x -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) )
11		ax-nul	|- E. s A. n -. n e. s
12		pm2.21	|- ( -. n e. s -> ( n e. s -> A. t -. t e. n ) )
13		alnex	|- ( A. n -. n e. s <-> -. E. n n e. s )
14		ifpfal	|- ( -. E. n n e. s -> ( if- ( E. n n e. s , w = x , w = y ) <-> w = y ) )
15	13 14	sylbi	|- ( A. n -. n e. s -> ( if- ( E. n n e. s , w = x , w = y ) <-> w = y ) )
16	11 12 15	axprlem4	|- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( w = y -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) )
17	10 16	jaod	|- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( ( w = x \/ w = y ) -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) )
18		imbi2	|- ( ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) -> ( ( ( w = x \/ w = y ) -> w e. z ) <-> ( ( w = x \/ w = y ) -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) ) )
19	17 18	syl5ibrcom	|- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) -> ( ( w = x \/ w = y ) -> w e. z ) ) )
20	19	alimdv	|- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( A. w ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) -> A. w ( ( w = x \/ w = y ) -> w e. z ) ) )
21	20	eximdv	|- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( E. z A. w ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) -> E. z A. w ( ( w = x \/ w = y ) -> w e. z ) ) )
22	1 21	mpi	|- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> E. z A. w ( ( w = x \/ w = y ) -> w e. z ) )
23		axprlem2	|- E. p A. s ( A. n e. s A. t -. t e. n -> s e. p )
24	22 23	exlimiiv	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )