Metamath Proof Explorer


Theorem nfeqd

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

Ref Expression
Hypotheses nfeqd.1 φ _ x A
nfeqd.2 φ _ x B
Assertion nfeqd φ x A = B

Proof

Step Hyp Ref Expression
1 nfeqd.1 φ _ x A
2 nfeqd.2 φ _ x B
3 dfcleq A = B y y A y B
4 nfv y φ
5 df-nfc _ x A y x y A
6 1 5 sylib φ y x y A
7 6 19.21bi φ x y A
8 df-nfc _ x B y x y B
9 2 8 sylib φ y x y B
10 9 19.21bi φ x y B
11 7 10 nfbid φ x y A y B
12 4 11 nfald φ x y y A y B
13 3 12 nfxfrd φ x A = B