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

Metamath Proof Explorer

Theorem nfrmod

Description: Deduction version of nfrmo . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 17-Jun-2017) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	nfrmod.1	$⊢ Ⅎ y φ$
		nfrmod.2	$⊢ φ \to \underline{Ⅎ} x A$
		nfrmod.3	$⊢ φ \to Ⅎ x ψ$
	Assertion	nfrmod	$⊢ φ \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-rmo	$⊢ \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	nfmod2	$⊢ φ \to Ⅎ x \exists^{*} y (y \in A \land ψ)$
12	4 11	nfxfrd	$⊢ φ \to Ⅎ x \exists^{*} y \in A ψ$