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	|- F/_ x A
	nfeq.2	|- F/_ x B
Assertion	nfeq	|- F/ x A = B

Proof

Step	Hyp	Ref	Expression
1		nfnfc.1	|- F/_ x A
2		nfeq.2	|- F/_ x B
3	1	a1i	|- ( T. -> F/_ x A )
4	2	a1i	|- ( T. -> F/_ x B )
5	3 4	nfeqd	|- ( T. -> F/ x A = B )
6	5	mptru	|- F/ x A = B