Theorem zfausclOLD

Description: Obsolete version of sepgi as of 14-Jul-2026. (Contributed by NM, 21-Jun-1993) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		sepgi.1	|- A e. _V
2		eleq2	|- ( z = A -> ( x e. z <-> x e. A ) )
3	2	anbi1d	|- ( z = A -> ( ( x e. z /\ ph ) <-> ( x e. A /\ ph ) ) )
4	3	bibi2d	|- ( z = A -> ( ( x e. y <-> ( x e. z /\ ph ) ) <-> ( x e. y <-> ( x e. A /\ ph ) ) ) )
5	4	albidv	|- ( z = A -> ( A. x ( x e. y <-> ( x e. z /\ ph ) ) <-> A. x ( x e. y <-> ( x e. A /\ ph ) ) ) )
6	5	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 ) ) ) )
7		ax-sep	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
8	1 6 7	vtocl	|- E. y A. x ( x e. y <-> ( x e. A /\ ph ) )