Theorem bj-sepg

Description: Version of sepg which does not require df-clab , thanks to the use of bj-vtoclg (and ultimately, to the use of elissetv instead of elisset ). This axiom save is not very important, since this theorem uses df-cleq and df-clel . This theorem is a remnant of a previous state of set.mm where the axiom saving was larger. (Contributed by BJ, 2-Jul-2022) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-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	biimpd	|- ( z = A -> ( ( x e. y <-> ( x e. z /\ ph ) ) -> ( x e. y <-> ( x e. A /\ ph ) ) ) )
5	4	alimdv	|- ( z = A -> ( A. x ( x e. y <-> ( x e. z /\ ph ) ) -> A. x ( x e. y <-> ( x e. A /\ ph ) ) ) )
6	5	eximdv	|- ( 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	6 7	bj-vtoclg	|- ( A e. V -> E. y A. x ( x e. y <-> ( x e. A /\ ph ) ) )