Theorem nfeq

Description: Hypothesis builder for equality. (Contributed by NM, 21-Jun-1993) (Revised by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 16-Nov-2019)

	Ref	Expression
Hypotheses	nfnfc.1	$$⊢\underset{\_}{Ⅎ}xA$$
	nfeq.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nfeq	$$⊢ℲxA=B$$

Proof

Step	Hyp	Ref	Expression
1		nfnfc.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfeq.2	$$⊢\underset{\_}{Ⅎ}xB$$
3	1	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xA$$
4	2	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xB$$
5	3 4	nfeqd	$$⊢\top \to ℲxA=B$$
6	5	mptru	$$⊢ℲxA=B$$