Metamath Proof Explorer

Theorem zfrepclf

Description: An inference based on the Axiom of Replacement. Typically, ph defines a function from x to y . (Contributed by NM, 26-Nov-1995)

		Ref	Expression
	Hypotheses	zfrepclf.1	$⊢ \underline{Ⅎ} x A$
		zfrepclf.2	$⊢ A \in V$
		zfrepclf.3	$⊢ x \in A \to \exists z \forall y (φ \to y = z)$
	Assertion	zfrepclf	$⊢ \exists z \forall y (y \in z \leftrightarrow \exists x (x \in A \land φ))$

Proof

Step	Hyp	Ref	Expression
1		zfrepclf.1	$⊢ \underline{Ⅎ} x A$
2		zfrepclf.2	$⊢ A \in V$
3		zfrepclf.3	$⊢ x \in A \to \exists z \forall y (φ \to y = z)$
4	1	nfeq2	$⊢ Ⅎ x v = A$
5		eleq2	$⊢ v = A \to (x \in v \leftrightarrow x \in A)$
6	5 3	syl6bi	$⊢ v = A \to (x \in v \to \exists z \forall y (φ \to y = z))$
7	4 6	alrimi	$⊢ v = A \to \forall x (x \in v \to \exists z \forall y (φ \to y = z))$
8		nfv	$⊢ Ⅎ z φ$
9	8	axrep5	$⊢ \forall x (x \in v \to \exists z \forall y (φ \to y = z)) \to \exists z \forall y (y \in z \leftrightarrow \exists x (x \in v \land φ))$
10	7 9	syl	$⊢ v = A \to \exists z \forall y (y \in z \leftrightarrow \exists x (x \in v \land φ))$
11	5	anbi1d	$⊢ v = A \to ((x \in v \land φ) \leftrightarrow (x \in A \land φ))$
12	4 11	exbid	$⊢ v = A \to (\exists x (x \in v \land φ) \leftrightarrow \exists x (x \in A \land φ))$
13	12	bibi2d	$⊢ v = A \to ((y \in z \leftrightarrow \exists x (x \in v \land φ)) \leftrightarrow (y \in z \leftrightarrow \exists x (x \in A \land φ)))$
14	13	albidv	$⊢ v = A \to (\forall y (y \in z \leftrightarrow \exists x (x \in v \land φ)) \leftrightarrow \forall y (y \in z \leftrightarrow \exists x (x \in A \land φ)))$
15	14	exbidv	$⊢ v = A \to (\exists z \forall y (y \in z \leftrightarrow \exists x (x \in v \land φ)) \leftrightarrow \exists z \forall y (y \in z \leftrightarrow \exists x (x \in A \land φ)))$
16	10 15	mpbid	$⊢ v = A \to \exists z \forall y (y \in z \leftrightarrow \exists x (x \in A \land φ))$
17	2 16	vtocle	$⊢ \exists z \forall y (y \in z \leftrightarrow \exists x (x \in A \land φ))$