Theorem nfned

Description: Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007) (Revised by Mario Carneiro, 7-Oct-2016)

	Ref	Expression
Hypotheses	nfned.1	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
	nfned.2	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
Assertion	nfned	$$⊢\phi \to ℲxA\ne B$$

Proof

Step	Hyp	Ref	Expression
1		nfned.1	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
2		nfned.2	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
3		df-ne	$$⊢A\ne B\leftrightarrow \neg A=B$$
4	1 2	nfeqd	$$⊢\phi \to ℲxA=B$$
5	4	nfnd	$$⊢\phi \to Ⅎx\neg A=B$$
6	3 5	nfxfrd	$$⊢\phi \to ℲxA\ne B$$