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

Metamath Proof Explorer

Theorem nfreud

Description: Deduction version of nfreu . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 15-Feb-2013) (Revised by Mario Carneiro, 8-Oct-2016) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	nfrmod.1	$⊢ Ⅎ y φ$
		nfrmod.2	$⊢ φ \to \underline{Ⅎ} x A$
		nfrmod.3	$⊢ φ \to Ⅎ x ψ$
	Assertion	nfreud	$⊢ φ \to Ⅎ x \exists! y \in A ψ$

Proof

Step	Hyp	Ref	Expression
1		nfrmod.1	$⊢ Ⅎ y φ$
2		nfrmod.2	$⊢ φ \to \underline{Ⅎ} x A$
3		nfrmod.3	$⊢ φ \to Ⅎ x ψ$
4		df-reu	$⊢ \exists! y \in A ψ \leftrightarrow \exists! y (y \in A \land ψ)$
5		nfcvf	$⊢ \neg \forall x x = y \to \underline{Ⅎ} x y$
6	5	adantl	$⊢ (φ \land \neg \forall x x = y) \to \underline{Ⅎ} x y$
7	2	adantr	$⊢ (φ \land \neg \forall x x = y) \to \underline{Ⅎ} x A$
8	6 7	nfeld	$⊢ (φ \land \neg \forall x x = y) \to Ⅎ x y \in A$
9	3	adantr	$⊢ (φ \land \neg \forall x x = y) \to Ⅎ x ψ$
10	8 9	nfand	$⊢ (φ \land \neg \forall x x = y) \to Ⅎ x (y \in A \land ψ)$
11	1 10	nfeud2	$⊢ φ \to Ⅎ x \exists! y (y \in A \land ψ)$
12	4 11	nfxfrd	$⊢ φ \to Ⅎ x \exists! y \in A ψ$