Metamath Proof Explorer

Theorem axsepg2

Description: A generalization of ax-sep in which x and z need not be distinct. This theorem scheme bundles ax-sep with the degenerate instance E. y A. z ( z e. y <-> ( z e. z /\ ph ) ) which is satisfied by the existence of the empty set. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by BTernaryTau, 21-May-2026) (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/ y -. A. z z = x
2 nfnae 
 |-  F/ x -. A. z z = x
3 nfcvf 
 |-  ( -. A. z z = x -> F/_ z x )
4 nfcvd 
 |-  ( -. A. z z = x -> F/_ z y )
5 3 4 nfeld 
 |-  ( -. A. z z = x -> F/ z x e. y )
6 nfcvd 
 |-  ( -. A. z z = x -> F/_ z w )
7 3 6 nfeld 
 |-  ( -. A. z z = x -> F/ z x e. w )
8 nfvd 
 |-  ( -. A. z z = x -> F/ z ph )
9 7 8 nfand 
 |-  ( -. A. z z = x -> F/ z ( x e. w /\ ph ) )
10 5 9 nfbid 
 |-  ( -. A. z z = x -> F/ z ( x e. y <-> ( x e. w /\ ph ) ) )
11 2 10 nfald 
 |-  ( -. A. z z = x -> F/ z A. x ( x e. y <-> ( x e. w /\ ph ) ) )
12 1 11 nfexd 
 |-  ( -. A. z z = x -> F/ z E. y A. x ( x e. y <-> ( x e. w /\ ph ) ) )
13 nfvd 
 |-  ( -. A. z z = x -> F/ w E. y A. x ( x e. y <-> ( x e. z /\ ph ) ) )
14 dveeq2 
 |-  ( -. A. x x = z -> ( w = z -> A. x w = z ) )
15 14 naecoms 
 |-  ( -. A. z z = x -> ( w = z -> A. x w = z ) )
16 elequ2 
 |-  ( w = z -> ( x e. w <-> x e. z ) )
17 16 anbi1d 
 |-  ( w = z -> ( ( x e. w /\ ph ) <-> ( x e. z /\ ph ) ) )
18 17 bibi2d 
 |-  ( w = z -> ( ( x e. y <-> ( x e. w /\ ph ) ) <-> ( x e. y <-> ( x e. z /\ ph ) ) ) )
19 18 biimpd 
 |-  ( w = z -> ( ( x e. y <-> ( x e. w /\ ph ) ) -> ( x e. y <-> ( x e. z /\ ph ) ) ) )
20 19 al2imi 
 |-  ( A. x w = z -> ( A. x ( x e. y <-> ( x e. w /\ ph ) ) -> A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )
21 20 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 ) ) ) )
22 15 21 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 ) ) ) ) )
23 elequ1 
 |-  ( z = x -> ( z e. y <-> x e. y ) )
24 elequ1 
 |-  ( z = x -> ( z e. z <-> x e. z ) )
25 24 anbi1d 
 |-  ( z = x -> ( ( z e. z /\ ph ) <-> ( x e. z /\ ph ) ) )
26 23 25 bibi12d 
 |-  ( z = x -> ( ( z e. y <-> ( z e. z /\ ph ) ) <-> ( x e. y <-> ( x e. z /\ ph ) ) ) )
27 26 biimpd 
 |-  ( z = x -> ( ( z e. y <-> ( z e. z /\ ph ) ) -> ( x e. y <-> ( x e. z /\ ph ) ) ) )
28 27 al2imi 
 |-  ( A. z z = x -> ( A. z ( z e. y <-> ( z e. z /\ ph ) ) -> A. z ( x e. y <-> ( x e. z /\ ph ) ) ) )
29 axc11 
 |-  ( A. z z = x -> ( A. z ( x e. y <-> ( x e. z /\ ph ) ) -> A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )
30 28 29 syld 
 |-  ( A. z z = x -> ( A. z ( z e. y <-> ( z e. z /\ ph ) ) -> A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )
31 30 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 ) ) ) )
32 ax-sep 
 |-  E. y A. x ( x e. y <-> ( x e. w /\ ph ) )
33 32 ax-gen 
 |-  A. w E. y A. x ( x e. y <-> ( x e. w /\ ph ) )
34 ax-nul 
 |-  E. y A. z -. z e. y
35 elirrv 
 |-  -. z e. z
36 35 intnanr 
 |-  -. ( z e. z /\ ph )
37 36 nbn 
 |-  ( -. z e. y <-> ( z e. y <-> ( z e. z /\ ph ) ) )
38 37 biimpi 
 |-  ( -. z e. y -> ( z e. y <-> ( z e. z /\ ph ) ) )
39 38 alimi 
 |-  ( A. z -. z e. y -> A. z ( z e. y <-> ( z e. z /\ ph ) ) )
40 34 39 eximii 
 |-  E. y A. z ( z e. y <-> ( z e. z /\ ph ) )
41 40 ax-gen 
 |-  A. z E. y A. z ( z e. y <-> ( z e. z /\ ph ) )
42 12 13 22 31 33 41 dvelimalcasei 
 |-  A. z E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
43 42 spi 
 |-  E. y A. x ( x e. y <-> ( x e. z /\ ph ) )