Theorem sepg

Description: Version of the axiom of separation where the "containing set" is a class variable and the sethood assumption is in the antecedent. (Contributed by NM, 21-Jun-1993) Put sepgi in closed form. (Revised by BJ, 2-Jul-2022)

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

Proof

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