Metamath Proof Explorer

Theorem axsepg

Description: A more general version of the axiom scheme of separation ax-sep , where variable z can also occur (in addition to x ) in formula ph , which can therefore be thought of as ph ( x , z ) . This version is derived from the more restrictive ax-sep with no additional set theory axioms. Note that it was also derived from ax-rep but without ax-sep as axsepgfromrep . (Contributed by NM, 10-Dec-2006) (Proof shortened by Mario Carneiro, 17-Nov-2016) Remove dependency on ax-12 and ax-13 and shorten proof. (Revised by BJ, 6-Oct-2019)

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

 |-  ( w = z -> ( x e. w <-> x e. z ) )

 |-  ( w = z -> ( ( x e. w /\ ph ) <-> ( x e. z /\ ph ) ) )

 |-  ( w = z -> ( ( x e. y <-> ( x e. w /\ ph ) ) <-> ( x e. y <-> ( x e. z /\ ph ) ) ) )

 |-  ( w = z -> ( A. x ( x e. y <-> ( x e. w /\ ph ) ) <-> A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )

 |-  ( w = z -> ( E. y A. x ( x e. y <-> ( x e. w /\ ph ) ) <-> E. y A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )

 |-  E. y A. x ( x e. y <-> ( x e. w /\ ph ) )

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