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

Metamath Proof Explorer

Theorem axsepgfromrep

Description: A more general version axsepg of the axiom scheme of separation ax-sep derived from the axiom scheme of replacement ax-rep (and first-order logic). The extra generality consists in the absence of a disjoint variable condition on z , ph (that is, variable z may occur in formula ph ). See linked statements for more information. (Contributed by NM, 11-Sep-2006) Remove dependencies on ax-9 to ax-13 . (Revised by SN, 25-Sep-2023) Use ax-sep instead (or axsepg if the extra generality is needed). (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 axrep6 
 |-  ( A. w E* x ( w = x /\ ph ) -> E. y A. x ( x e. y <-> E. w e. z ( w = x /\ ph ) ) )
2 euequ 
 |-  E! x x = w
3 2 eumoi 
 |-  E* x x = w
4 equcomi 
 |-  ( w = x -> x = w )
5 4 adantr 
 |-  ( ( w = x /\ ph ) -> x = w )
6 5 moimi 
 |-  ( E* x x = w -> E* x ( w = x /\ ph ) )
7 3 6 ax-mp 
 |-  E* x ( w = x /\ ph )
8 1 7 mpg 
 |-  E. y A. x ( x e. y <-> E. w e. z ( w = x /\ ph ) )
9 df-rex 
 |-  ( E. w e. z ( w = x /\ ph ) <-> E. w ( w e. z /\ ( w = x /\ ph ) ) )
10 an12 
 |-  ( ( w = x /\ ( w e. z /\ ph ) ) <-> ( w e. z /\ ( w = x /\ ph ) ) )
11 10 exbii 
 |-  ( E. w ( w = x /\ ( w e. z /\ ph ) ) <-> E. w ( w e. z /\ ( w = x /\ ph ) ) )
12 elequ1 
 |-  ( w = x -> ( w e. z <-> x e. z ) )
13 12 anbi1d 
 |-  ( w = x -> ( ( w e. z /\ ph ) <-> ( x e. z /\ ph ) ) )
14 13 equsexvw 
 |-  ( E. w ( w = x /\ ( w e. z /\ ph ) ) <-> ( x e. z /\ ph ) )
15 9 11 14 3bitr2i 
 |-  ( E. w e. z ( w = x /\ ph ) <-> ( x e. z /\ ph ) )
16 15 bibi2i 
 |-  ( ( x e. y <-> E. w e. z ( w = x /\ ph ) ) <-> ( x e. y <-> ( x e. z /\ ph ) ) )
17 16 albii 
 |-  ( A. x ( x e. y <-> E. w e. z ( w = x /\ ph ) ) <-> A. x ( x e. y <-> ( x e. z /\ ph ) ) )
18 17 exbii 
 |-  ( E. y A. x ( x e. y <-> E. w e. z ( w = x /\ ph ) ) <-> E. y A. x ( x e. y <-> ( x e. z /\ ph ) ) )
19 8 18 mpbi 
 |-  E. y A. x ( x e. y <-> ( x e. z /\ ph ) )