Theorem nfeqd

Description: Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016)

	Ref	Expression
Hypotheses	nfeqd.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
	nfeqd.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
Assertion	nfeqd	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfeqd.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2		nfeqd.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
3		dfcleq	⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
4		nfv	⊢ Ⅎ 𝑦 𝜑
5	1	nfcrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 ∈ 𝐴 )
6	2	nfcrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 ∈ 𝐵 )
7	5 6	nfbid	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
8	4 7	nfald	⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
9	3 8	nfxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 = 𝐵 )