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

Metamath Proof Explorer

Theorem nfrmo

Description: Bound-variable hypothesis builder for restricted uniqueness. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfrmow when possible. (Contributed by NM, 16-Jun-2017) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	nfrmo.1	$⊢ \underline{Ⅎ} x A$
		nfrmo.2	$⊢ Ⅎ x φ$
	Assertion	nfrmo	$⊢ Ⅎ x \exists^{*} y \in A φ$

Proof

Step	Hyp	Ref	Expression
1		nfrmo.1	$⊢ \underline{Ⅎ} x A$
2		nfrmo.2	$⊢ Ⅎ x φ$
3		df-rmo	$⊢ \exists^{} y \in A φ \leftrightarrow \exists^{} y (y \in A \land φ)$
4		nftru	$⊢ Ⅎ y ⊤$
5		nfcvf	$⊢ \neg \forall x x = y \to \underline{Ⅎ} x y$
6	1	a1i	$⊢ \neg \forall x x = y \to \underline{Ⅎ} x A$
7	5 6	nfeld	$⊢ \neg \forall x x = y \to Ⅎ x y \in A$
8	2	a1i	$⊢ \neg \forall x x = y \to Ⅎ x φ$
9	7 8	nfand	$⊢ \neg \forall x x = y \to Ⅎ x (y \in A \land φ)$
10	9	adantl	$⊢ (⊤ \land \neg \forall x x = y) \to Ⅎ x (y \in A \land φ)$
11	4 10	nfmod2	$⊢ ⊤ \to Ⅎ x \exists^{*} y (y \in A \land φ)$
12	11	mptru	$⊢ Ⅎ x \exists^{*} y (y \in A \land φ)$
13	3 12	nfxfr	$⊢ Ⅎ x \exists^{*} y \in A φ$