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

Theorem nfeqd 2915
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 2730 . 2 (𝐴 = 𝐵 ↔ ∀𝑦(𝑦𝐴𝑦𝐵))
2 nfv 1917 . . 3 𝑦𝜑
3 nfeqd.1 . . . . . 6 (𝜑𝑥𝐴)
4 df-nfc 2887 . . . . . 6 (𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
53, 4sylib 217 . . . . 5 (𝜑 → ∀𝑦𝑥 𝑦𝐴)
6519.21bi 2182 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐴)
7 nfeqd.2 . . . . . 6 (𝜑𝑥𝐵)
8 df-nfc 2887 . . . . . 6 (𝑥𝐵 ↔ ∀𝑦𝑥 𝑦𝐵)
97, 8sylib 217 . . . . 5 (𝜑 → ∀𝑦𝑥 𝑦𝐵)
10919.21bi 2182 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐵)
116, 10nfbid 1905 . . 3 (𝜑 → Ⅎ𝑥(𝑦𝐴𝑦𝐵))
122, 11nfald 2322 . 2 (𝜑 → Ⅎ𝑥𝑦(𝑦𝐴𝑦𝐵))
131, 12nfxfrd 1856 1 (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1539   = wceq 1541  wnf 1785  wcel 2106  wnfc 2885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786  df-cleq 2729  df-nfc 2887
This theorem is referenced by:  nfeld  2916  nfeq  2918  nfned  3044  vtoclgft  3507  sbcralt  3826  csbiebt  3883  csbie2df  4398  dfnfc2  4888  eusvnfb  5346  eusv2i  5347  dfid3  5532  iota2df  6480  riotaeqimp  7334  riota5f  7336  oprabid  7383  axrepndlem1  10486  axrepndlem2  10487  axunnd  10490  axpowndlem4  10494  axregndlem2  10497  axinfndlem1  10499  axinfnd  10500  axacndlem4  10504  axacndlem5  10505  axacnd  10506  bj-elgab  35347  bj-gabima  35348  wl-issetft  35972  riotasv2d  37357  nfxnegd  43581
  Copyright terms: Public domain W3C validator