Theorem bj-zfauscl

Description: General version of zfauscl .

Remark: the comment in zfauscl is misleading: the essential use of ax-ext is the one via eleq2 and not the one via vtocl , since the latter can be proved without ax-ext (see bj-vtoclg ).

(Contributed by BJ, 2-Jul-2022) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-zfauscl	|- ( 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 ) ) )