Metamath Proof Explorer

Theorem axsepg2ALT

Description: Alternate proof of axsepg2 , derived directly from ax-sep with no additional set theory axioms. (Contributed by BTernaryTau, 3-Aug-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axsepg2ALT 
|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ x -. A. y y = z
2 nfvd 
 |-  ( -. A. y y = z -> F/ y x e. w )
3 nfcvf 
 |-  ( -. A. y y = z -> F/_ y z )
4 3 nfcrd 
 |-  ( -. A. y y = z -> F/ y x e. z )
5 nfvd 
 |-  ( -. A. y y = z -> F/ y ph )
6 4 5 nfand 
 |-  ( -. A. y y = z -> F/ y ( x e. z /\ ph ) )
7 2 6 nfbid 
 |-  ( -. A. y y = z -> F/ y ( x e. w <-> ( x e. z /\ ph ) ) )
8 1 7 nfald 
 |-  ( -. A. y y = z -> F/ y A. x ( x e. w <-> ( x e. z /\ ph ) ) )
9 nfvd 
 |-  ( -. A. y y = z -> F/ w A. x ( x e. y <-> ( x e. z /\ ph ) ) )
10 elequ2 
 |-  ( w = y -> ( x e. w <-> x e. y ) )
11 10 bibi1d 
 |-  ( w = y -> ( ( x e. w <-> ( x e. z /\ ph ) ) <-> ( x e. y <-> ( x e. z /\ ph ) ) ) )
12 11 biimpd 
 |-  ( w = y -> ( ( x e. w <-> ( x e. z /\ ph ) ) -> ( x e. y <-> ( x e. z /\ ph ) ) ) )
13 12 alimdv 
 |-  ( w = y -> ( A. x ( x e. w <-> ( x e. z /\ ph ) ) -> A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )
14 13 a1i 
 |-  ( -. A. y y = z -> ( w = y -> ( A. x ( x e. w <-> ( x e. z /\ ph ) ) -> A. x ( x e. y <-> ( x e. z /\ ph ) ) ) ) )
15 elequ2 
 |-  ( y = z -> ( x e. y <-> x e. z ) )
16 15 anbi1d 
 |-  ( y = z -> ( ( x e. y /\ ph ) <-> ( x e. z /\ ph ) ) )
17 16 bibi2d 
 |-  ( y = z -> ( ( x e. y <-> ( x e. y /\ ph ) ) <-> ( x e. y <-> ( x e. z /\ ph ) ) ) )
18 17 biimpd 
 |-  ( y = z -> ( ( x e. y <-> ( x e. y /\ ph ) ) -> ( x e. y <-> ( x e. z /\ ph ) ) ) )
19 18 alimdv 
 |-  ( y = z -> ( A. x ( x e. y <-> ( x e. y /\ ph ) ) -> A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )
20 19 sps 
 |-  ( A. y y = z -> ( A. x ( x e. y <-> ( x e. y /\ ph ) ) -> A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )
21 ax-sep 
 |-  E. w A. x ( x e. w <-> ( x e. z /\ ph ) )
22 ax-sep 
 |-  E. y A. x ( x e. y <-> ( x e. v /\ F. ) )
23 fal 
 |-  -. F.
24 23 intnan 
 |-  -. ( x e. v /\ F. )
25 biimp 
 |-  ( ( x e. y <-> ( x e. v /\ F. ) ) -> ( x e. y -> ( x e. v /\ F. ) ) )
26 24 25 mtoi 
 |-  ( ( x e. y <-> ( x e. v /\ F. ) ) -> -. x e. y )
27 26 bianfd 
 |-  ( ( x e. y <-> ( x e. v /\ F. ) ) -> ( x e. y <-> ( x e. y /\ ph ) ) )
28 27 alimi 
 |-  ( A. x ( x e. y <-> ( x e. v /\ F. ) ) -> A. x ( x e. y <-> ( x e. y /\ ph ) ) )
29 22 28 eximii 
 |-  E. y A. x ( x e. y <-> ( x e. y /\ ph ) )
30 8 9 14 20 21 29 dvelimexcasei 
 |-  E. y A. x ( x e. y <-> ( x e. z /\ ph ) )