This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )