Theorem axprg

Description: Derive The Axiom of Pairing with class variables. (Contributed by GG, 6-Mar-2026)

	Ref	Expression
Assertion	axprg	|- E. z A. w ( ( w = A \/ w = B ) -> w e. z )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	|- ( w = x -> ( w = A <-> x = A ) )
2		eqeq1	|- ( w = x -> ( w = B <-> x = B ) )
3	1 2	orbi12d	|- ( w = x -> ( ( w = A \/ w = B ) <-> ( x = A \/ x = B ) ) )
4	3	cbvexvw	|- ( E. w ( w = A \/ w = B ) <-> E. x ( x = A \/ x = B ) )
5		axprglem	|- ( x = A -> E. z A. w ( ( w = A \/ w = B ) -> w e. z ) )
6		axprglem	|- ( x = B -> E. z A. w ( ( w = B \/ w = A ) -> w e. z ) )
7		pm1.4	|- ( ( w = A \/ w = B ) -> ( w = B \/ w = A ) )
8	7	imim1i	|- ( ( ( w = B \/ w = A ) -> w e. z ) -> ( ( w = A \/ w = B ) -> w e. z ) )
9	8	alimi	|- ( A. w ( ( w = B \/ w = A ) -> w e. z ) -> A. w ( ( w = A \/ w = B ) -> w e. z ) )
10	9	eximi	|- ( E. z A. w ( ( w = B \/ w = A ) -> w e. z ) -> E. z A. w ( ( w = A \/ w = B ) -> w e. z ) )
11	6 10	syl	|- ( x = B -> E. z A. w ( ( w = A \/ w = B ) -> w e. z ) )
12	5 11	jaoi	|- ( ( x = A \/ x = B ) -> E. z A. w ( ( w = A \/ w = B ) -> w e. z ) )
13	12	exlimiv	|- ( E. x ( x = A \/ x = B ) -> E. z A. w ( ( w = A \/ w = B ) -> w e. z ) )
14	4 13	sylbi	|- ( E. w ( w = A \/ w = B ) -> E. z A. w ( ( w = A \/ w = B ) -> w e. z ) )
15		alnex	|- ( A. w -. ( w = A \/ w = B ) <-> -. E. w ( w = A \/ w = B ) )
16		pm2.21	|- ( -. ( w = A \/ w = B ) -> ( ( w = A \/ w = B ) -> w e. z ) )
17	16	alimi	|- ( A. w -. ( w = A \/ w = B ) -> A. w ( ( w = A \/ w = B ) -> w e. z ) )
18	15 17	sylbir	|- ( -. E. w ( w = A \/ w = B ) -> A. w ( ( w = A \/ w = B ) -> w e. z ) )
19	18	exgen	|- E. z ( -. E. w ( w = A \/ w = B ) -> A. w ( ( w = A \/ w = B ) -> w e. z ) )
20	19	19.37iv	|- ( -. E. w ( w = A \/ w = B ) -> E. z A. w ( ( w = A \/ w = B ) -> w e. z ) )
21	14 20	pm2.61i	|- E. z A. w ( ( w = A \/ w = B ) -> w e. z )