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)

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

Proof

Step	Hyp	Ref	Expression
1		elequ2	|- ( w = z -> ( x e. w <-> x e. z ) )
2	1	anbi1d	|- ( w = z -> ( ( x e. w /\ ph ) <-> ( x e. z /\ ph ) ) )
3	2	bibi2d	|- ( w = z -> ( ( x e. y <-> ( x e. w /\ ph ) ) <-> ( x e. y <-> ( x e. z /\ ph ) ) ) )
4	3	albidv	|- ( w = z -> ( A. x ( x e. y <-> ( x e. w /\ ph ) ) <-> A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )
5	4	exbidv	|- ( w = z -> ( E. y A. x ( x e. y <-> ( x e. w /\ ph ) ) <-> E. y A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )
6		ax-sep	|- E. y A. x ( x e. y <-> ( x e. w /\ ph ) )
7	5 6	chvarvv	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )