MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfeqd Structured version   Visualization version   GIF version

Theorem nfeqd 2769
Description: Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.)
Hypotheses
Ref Expression
nfeqd.1 (𝜑𝑥𝐴)
nfeqd.2 (𝜑𝑥𝐵)
Assertion
Ref Expression
nfeqd (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)

Proof of Theorem nfeqd
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2614 . 2 (𝐴 = 𝐵 ↔ ∀𝑦(𝑦𝐴𝑦𝐵))
2 nfv 1841 . . 3 𝑦𝜑
3 nfeqd.1 . . . . 5 (𝜑𝑥𝐴)
43nfcrd 2768 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐴)
5 nfeqd.2 . . . . 5 (𝜑𝑥𝐵)
65nfcrd 2768 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐵)
74, 6nfbid 1830 . . 3 (𝜑 → Ⅎ𝑥(𝑦𝐴𝑦𝐵))
82, 7nfald 2163 . 2 (𝜑 → Ⅎ𝑥𝑦(𝑦𝐴𝑦𝐵))
91, 8nfxfrd 1778 1 (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1479   = wceq 1481  wnf 1706  wcel 1988  wnfc 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1703  df-nf 1708  df-cleq 2613  df-nfc 2751
This theorem is referenced by:  nfeld  2770  nfeq  2773  nfned  2892  vtoclgft  3249  vtoclgftOLD  3250  sbcralt  3504  csbiebt  3546  dfnfc2  4445  dfnfc2OLD  4446  eusvnfb  4853  eusv2i  4854  dfid3  5015  iota2df  5863  riotaeqimp  6619  riota5f  6621  oprabid  6662  axrepndlem1  9399  axrepndlem2  9400  axunnd  9403  axpowndlem4  9407  axregndlem2  9410  axinfndlem1  9412  axinfnd  9413  axacndlem4  9417  axacndlem5  9418  axacnd  9419  riotasv2d  34062  nfxnegd  39481
  Copyright terms: Public domain W3C validator