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

Metamath Proof Explorer

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	⊢ Ⅎ 𝑥 𝐴
	nfeq.2	⊢ Ⅎ 𝑥 𝐵
Assertion	nfeq	⊢ Ⅎ 𝑥 𝐴 = 𝐵

Proof

Step	Hyp	Ref	Expression
1		nfnfc.1	⊢ Ⅎ 𝑥 𝐴
2		nfeq.2	⊢ Ⅎ 𝑥 𝐵
3	1	a1i	⊢ ( ⊤ → Ⅎ 𝑥 𝐴 )
4	2	a1i	⊢ ( ⊤ → Ⅎ 𝑥 𝐵 )
5	3 4	nfeqd	⊢ ( ⊤ → Ⅎ 𝑥 𝐴 = 𝐵 )
6	5	mptru	⊢ Ⅎ 𝑥 𝐴 = 𝐵