Metamath Proof Explorer


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 ( 𝜑 → Ⅎ 𝑥 𝐴 = 𝐵 )