# Metamath Proof Explorer

## Theorem nfeqd

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

Ref Expression
Hypotheses nfeqd.1 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
nfeqd.2 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
Assertion nfeqd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}={B}$

### Proof

Step Hyp Ref Expression
1 nfeqd.1 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 nfeqd.2 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
3 dfcleq ${⊢}{A}={B}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}↔{y}\in {B}\right)$
4 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
5 1 nfcrd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {A}$
6 2 nfcrd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
7 5 6 nfbid ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}↔{y}\in {B}\right)$
8 4 7 nfald ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}↔{y}\in {B}\right)$
9 3 8 nfxfrd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}={B}$