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

Theorem nfeqd 2929
 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 2751 . 2 (𝐴 = 𝐵 ↔ ∀𝑦(𝑦𝐴𝑦𝐵))
2 nfv 1915 . . 3 𝑦𝜑
3 nfeqd.1 . . . . . 6 (𝜑𝑥𝐴)
4 df-nfc 2901 . . . . . 6 (𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
53, 4sylib 221 . . . . 5 (𝜑 → ∀𝑦𝑥 𝑦𝐴)
6519.21bi 2186 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐴)
7 nfeqd.2 . . . . . 6 (𝜑𝑥𝐵)
8 df-nfc 2901 . . . . . 6 (𝑥𝐵 ↔ ∀𝑦𝑥 𝑦𝐵)
97, 8sylib 221 . . . . 5 (𝜑 → ∀𝑦𝑥 𝑦𝐵)
10919.21bi 2186 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐵)
116, 10nfbid 1903 . . 3 (𝜑 → Ⅎ𝑥(𝑦𝐴𝑦𝐵))
122, 11nfald 2336 . 2 (𝜑 → Ⅎ𝑥𝑦(𝑦𝐴𝑦𝐵))
131, 12nfxfrd 1855 1 (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   = wceq 1538  Ⅎwnf 1785   ∈ wcel 2111  Ⅎwnfc 2899 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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-cleq 2750  df-nfc 2901 This theorem is referenced by:  nfeld  2930  nfeq  2932  nfned  3052  vtoclgft  3472  vtoclgftOLD  3473  sbcralt  3780  csbiebt  3836  csbie2df  4340  dfnfc2  4825  eusvnfb  5265  eusv2i  5266  dfid3  5435  iota2df  6326  riotaeqimp  7139  riota5f  7141  oprabid  7187  axrepndlem1  10057  axrepndlem2  10058  axunnd  10061  axpowndlem4  10065  axregndlem2  10068  axinfndlem1  10070  axinfnd  10071  axacndlem4  10075  axacndlem5  10076  axacnd  10077  riotasv2d  36559  nfxnegd  42472
 Copyright terms: Public domain W3C validator