Metamath Proof Explorer

Theorem axsepg4

Description: A generalization of ax-sep that combines axsepg and axsepg2 into a single theorem scheme. Unlike ax-sep , this scheme lacks a distinct variable condition for ph and z as well as for x and z . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by BTernaryTau, 24-May-2026) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nfa1 
 |-  F/ z A. z E. y A. x ( x e. y <-> ( x e. w /\ ph ) )
2 1 a1i 
 |-  ( -. A. z z = x -> F/ z A. z E. y A. x ( x e. y <-> ( x e. w /\ ph ) ) )
3 nfvd 
 |-  ( -. A. z z = x -> F/ w E. y A. x ( x e. y <-> ( x e. z /\ ph ) ) )
4 sp 
 |-  ( A. z E. y A. x ( x e. y <-> ( x e. w /\ ph ) ) -> E. y A. x ( x e. y <-> ( x e. w /\ ph ) ) )
5 dveeq2 
 |-  ( -. A. x x = z -> ( w = z -> A. x w = z ) )
6 5 naecoms 
 |-  ( -. A. z z = x -> ( w = z -> A. x w = z ) )
7 elequ2 
 |-  ( w = z -> ( x e. w <-> x e. z ) )
8 7 anbi1d 
 |-  ( w = z -> ( ( x e. w /\ ph ) <-> ( x e. z /\ ph ) ) )
9 8 bibi2d 
 |-  ( w = z -> ( ( x e. y <-> ( x e. w /\ ph ) ) <-> ( x e. y <-> ( x e. z /\ ph ) ) ) )
10 9 biimpd 
 |-  ( w = z -> ( ( x e. y <-> ( x e. w /\ ph ) ) -> ( x e. y <-> ( x e. z /\ ph ) ) ) )
11 10 al2imi 
 |-  ( A. x w = z -> ( A. x ( x e. y <-> ( x e. w /\ ph ) ) -> A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )
12 11 eximdv 
 |-  ( A. x w = z -> ( E. y A. x ( x e. y <-> ( x e. w /\ ph ) ) -> E. y A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )
13 6 12 syl6 
 |-  ( -. A. z z = x -> ( w = z -> ( E. y A. x ( x e. y <-> ( x e. w /\ ph ) ) -> E. y A. x ( x e. y <-> ( x e. z /\ ph ) ) ) ) )
14 4 13 syl7 
 |-  ( -. A. z z = x -> ( w = z -> ( A. z E. y A. x ( x e. y <-> ( x e. w /\ ph ) ) -> E. y A. x ( x e. y <-> ( x e. z /\ ph ) ) ) ) )
15 elequ1 
 |-  ( z = x -> ( z e. y <-> x e. y ) )
16 elequ1 
 |-  ( z = x -> ( z e. z <-> x e. z ) )
17 16 anbi1d 
 |-  ( z = x -> ( ( z e. z /\ ph ) <-> ( x e. z /\ ph ) ) )
18 15 17 bibi12d 
 |-  ( z = x -> ( ( z e. y <-> ( z e. z /\ ph ) ) <-> ( x e. y <-> ( x e. z /\ ph ) ) ) )
19 18 biimpd 
 |-  ( z = x -> ( ( z e. y <-> ( z e. z /\ ph ) ) -> ( x e. y <-> ( x e. z /\ ph ) ) ) )
20 19 al2imi 
 |-  ( A. z z = x -> ( A. z ( z e. y <-> ( z e. z /\ ph ) ) -> A. z ( x e. y <-> ( x e. z /\ ph ) ) ) )
21 axc11 
 |-  ( A. z z = x -> ( A. z ( x e. y <-> ( x e. z /\ ph ) ) -> A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )
22 20 21 syld 
 |-  ( A. z z = x -> ( A. z ( z e. y <-> ( z e. z /\ ph ) ) -> A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )
23 22 eximdv 
 |-  ( A. z z = x -> ( E. y A. z ( z e. y <-> ( z e. z /\ ph ) ) -> E. y A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )
24 axsepg 
 |-  E. y A. x ( x e. y <-> ( x e. w /\ ph ) )
25 24 gen2 
 |-  A. w A. z E. y A. x ( x e. y <-> ( x e. w /\ ph ) )
26 ax-nul 
 |-  E. y A. z -. z e. y
27 elirrv 
 |-  -. z e. z
28 27 intnanr 
 |-  -. ( z e. z /\ ph )
29 28 nbn 
 |-  ( -. z e. y <-> ( z e. y <-> ( z e. z /\ ph ) ) )
30 29 biimpi 
 |-  ( -. z e. y -> ( z e. y <-> ( z e. z /\ ph ) ) )
31 30 alimi 
 |-  ( A. z -. z e. y -> A. z ( z e. y <-> ( z e. z /\ ph ) ) )
32 26 31 eximii 
 |-  E. y A. z ( z e. y <-> ( z e. z /\ ph ) )
33 32 ax-gen 
 |-  A. z E. y A. z ( z e. y <-> ( z e. z /\ ph ) )
34 2 3 14 23 25 33 dvelimalcasei 
 |-  A. z E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
35 34 spi 
 |-  E. y A. x ( x e. y <-> ( x e. z /\ ph ) )