This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zfrep3cl

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	zfrep3cl.1	$⊢ A \in V$
	zfrep3cl.2	$⊢ x \in A \to \exists z \forall y (φ \to y = z)$
Assertion	zfrep3cl	$⊢ \exists z \forall y (y \in z \leftrightarrow \exists x (x \in A \land φ))$

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