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) 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		biimpr	|- ( ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) -> ( E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) -> w e. z ) )
3	2	alimi	|- ( A. w ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) -> A. w ( E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) -> w e. z ) )
4	1 3	eximii	|- E. z A. w ( E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) -> w e. z )
5		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 ) ) )
6		axprlem5	|- ( ( 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 ) ) )
7	5 6	jaodan	|- ( ( 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 ) ) )
8	7	ex	|- ( 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 ) ) ) )
9	8	imim1d	|- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( ( E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) -> w e. z ) -> ( ( w = x \/ w = y ) -> w e. z ) ) )
10	9	alimdv	|- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( A. w ( E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) -> w e. z ) -> A. w ( ( w = x \/ w = y ) -> w e. z ) ) )
11	10	eximdv	|- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( E. z A. w ( E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) -> w e. z ) -> E. z A. w ( ( w = x \/ w = y ) -> w e. z ) ) )
12	4 11	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 ) )
13		axprlem2	|- E. p A. s ( A. n e. s A. t -. t e. n -> s e. p )
14	12 13	exlimiiv	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )