Metamath Proof Explorer

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 \in V \to \exists y \forall x (x \in y \leftrightarrow (x \in A \land φ))$

Proof

Step	Hyp	Ref	Expression
1		eleq2	$⊢ z = A \to (x \in z \leftrightarrow x \in A)$
2	1	anbi1d	$⊢ z = A \to ((x \in z \land φ) \leftrightarrow (x \in A \land φ))$
3	2	bibi2d	$⊢ z = A \to ((x \in y \leftrightarrow (x \in z \land φ)) \leftrightarrow (x \in y \leftrightarrow (x \in A \land φ)))$
4	3	biimpd	$⊢ z = A \to ((x \in y \leftrightarrow (x \in z \land φ)) \to (x \in y \leftrightarrow (x \in A \land φ)))$
5	4	alimdv	$⊢ z = A \to (\forall x (x \in y \leftrightarrow (x \in z \land φ)) \to \forall x (x \in y \leftrightarrow (x \in A \land φ)))$
6	5	eximdv	$⊢ z = A \to (\exists y \forall x (x \in y \leftrightarrow (x \in z \land φ)) \to \exists y \forall x (x \in y \leftrightarrow (x \in A \land φ)))$
7		ax-sep	$⊢ \exists y \forall x (x \in y \leftrightarrow (x \in z \land φ))$
8	6 7	bj-vtoclg	$⊢ A \in V \to \exists y \forall x (x \in y \leftrightarrow (x \in A \land φ))$