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

Theorem nfeqd 2906
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 2726 . 2 (𝐴 = 𝐵 ↔ ∀𝑦(𝑦𝐴𝑦𝐵))
2 nfv 1915 . . 3 𝑦𝜑
3 nfeqd.1 . . . . . 6 (𝜑𝑥𝐴)
4 df-nfc 2882 . . . . . 6 (𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
53, 4sylib 218 . . . . 5 (𝜑 → ∀𝑦𝑥 𝑦𝐴)
6519.21bi 2194 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐴)
7 nfeqd.2 . . . . . 6 (𝜑𝑥𝐵)
8 df-nfc 2882 . . . . . 6 (𝑥𝐵 ↔ ∀𝑦𝑥 𝑦𝐵)
97, 8sylib 218 . . . . 5 (𝜑 → ∀𝑦𝑥 𝑦𝐵)
10919.21bi 2194 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐵)
116, 10nfbid 1903 . . 3 (𝜑 → Ⅎ𝑥(𝑦𝐴𝑦𝐵))
122, 11nfald 2331 . 2 (𝜑 → Ⅎ𝑥𝑦(𝑦𝐴𝑦𝐵))
131, 12nfxfrd 1855 1 (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1539   = wceq 1541  wnf 1784  wcel 2113  wnfc 2880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-cleq 2725  df-nfc 2882
This theorem is referenced by:  nfeld  2907  nfeq  2909  nfned  3031  cbvexeqsetf  3452  sbcralt  3819  csbiebt  3875  csbie2df  4392  dfnfc2  4880  eusvnfb  5333  eusv2i  5334  dfid3  5517  iota2df  6473  riotaeqimp  7335  riota5f  7337  oprabid  7384  axrepndlem1  10490  axrepndlem2  10491  axunnd  10494  axpowndlem4  10498  axregndlem2  10501  axinfndlem1  10503  axinfnd  10504  axacndlem4  10508  axacndlem5  10509  axacnd  10510  bj-elgab  37004  bj-gabima  37005  wl-issetft  37647  riotasv2d  39076  nfxnegd  45563
  Copyright terms: Public domain W3C validator