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	$$⊢\underset{\_}{Ⅎ}xA$$
	nfrmo.2	$$⊢Ⅎx\phi$$
Assertion	nfrmo	$$⊢Ⅎx{\exists }^{*}y\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		nfrmo.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfrmo.2	$$⊢Ⅎx\phi$$
3		df-rmo	$$⊢{\exists }^{*}y\in A\phi \leftrightarrow {\exists }^{*}y\left(y\in A\wedge \phi \right)$$
4		nftru	$$⊢Ⅎy\top$$
5		nfcvf	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}xy$$
6	1	a1i	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}xA$$
7	5 6	nfeld	$$⊢\neg \forall xx=y\to Ⅎxy\in A$$
8	2	a1i	$$⊢\neg \forall xx=y\to Ⅎx\phi$$
9	7 8	nfand	$$⊢\neg \forall xx=y\to Ⅎx\left(y\in A\wedge \phi \right)$$
10	9	adantl	$$⊢\left(\top \wedge \neg \forall xx=y\right)\to Ⅎx\left(y\in A\wedge \phi \right)$$
11	4 10	nfmod2	$$⊢\top \to Ⅎx{\exists }^{*}y\left(y\in A\wedge \phi \right)$$
12	11	mptru	$$⊢Ⅎx{\exists }^{*}y\left(y\in A\wedge \phi \right)$$
13	3 12	nfxfr	$$⊢Ⅎx{\exists }^{*}y\in A\phi$$