Metamath Proof Explorer

Theorem axsepg2

Description: A generalization of ax-sep in which y and z need not be distinct. See also axsepg which instead allows z to occur in ph . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by BTernaryTau, 3-Aug-2025) (New usage is discouraged.)

Ref Expression
Assertion axsepg2 
|- 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-nul 
 |-  E. y A. x -. x e. y
23 id 
 |-  ( -. x e. y -> -. x e. y )
24 23 bianfd 
 |-  ( -. x e. y -> ( x e. y <-> ( x e. y /\ ph ) ) )
25 24 alimi 
 |-  ( A. x -. x e. y -> A. x ( x e. y <-> ( x e. y /\ ph ) ) )
26 22 25 eximii 
 |-  E. y A. x ( x e. y <-> ( x e. y /\ ph ) )
27 8 9 14 20 21 26 dvelimexcasei 
 |-  E. y A. x ( x e. y <-> ( x e. z /\ ph ) )