Theorem sepgi

Description: Inference associated with sepg . The requirement that y not occur in ph is necessary, as notsep shows. (Contributed by NM, 21-Jun-1993) (Revised by BJ, 14-Jul-2026)

	Ref	Expression
Hypothesis	sepgi.1	|- A e. _V
Assertion	sepgi	|- E. y A. x ( x e. y <-> ( x e. A /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		sepgi.1	|- A e. _V
2		sepg	|- ( A e. _V -> E. y A. x ( x e. y <-> ( x e. A /\ ph ) ) )
3	1 2	ax-mp	|- E. y A. x ( x e. y <-> ( x e. A /\ ph ) )