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		df-nfc	⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 )
6	1 5	sylib	⊢ ( 𝜑 → ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 )
7	6	19.21bi	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 ∈ 𝐴 )
8		df-nfc	⊢ ( Ⅎ 𝑥 𝐵 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐵 )
9	2 8	sylib	⊢ ( 𝜑 → ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐵 )
10	9	19.21bi	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 ∈ 𝐵 )
11	7 10	nfbid	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
12	4 11	nfald	⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
13	3 12	nfxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 = 𝐵 )