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

Theorem nfeqd 2985
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 2812 . 2 (𝐴 = 𝐵 ↔ ∀𝑦(𝑦𝐴𝑦𝐵))
2 nfv 1906 . . 3 𝑦𝜑
3 nfeqd.1 . . . . 5 (𝜑𝑥𝐴)
43nfcrd 2966 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐴)
5 nfeqd.2 . . . . 5 (𝜑𝑥𝐵)
65nfcrd 2966 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐵)
74, 6nfbid 1894 . . 3 (𝜑 → Ⅎ𝑥(𝑦𝐴𝑦𝐵))
82, 7nfald 2338 . 2 (𝜑 → Ⅎ𝑥𝑦(𝑦𝐴𝑦𝐵))
91, 8nfxfrd 1845 1 (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1526   = wceq 1528  wnf 1775  wcel 2105  wnfc 2958
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-ex 1772  df-nf 1776  df-cleq 2811  df-nfc 2960
This theorem is referenced by:  nfeld  2986  nfeq  2988  nfned  3117  vtoclgft  3551  vtoclgftOLD  3552  sbcralt  3852  csbiebt  3909  dfnfc2  4848  eusvnfb  5284  eusv2i  5285  dfid3  5455  iota2df  6335  riotaeqimp  7129  riota5f  7131  oprabid  7177  axrepndlem1  10002  axrepndlem2  10003  axunnd  10006  axpowndlem4  10010  axregndlem2  10013  axinfndlem1  10015  axinfnd  10016  axacndlem4  10020  axacndlem5  10021  axacnd  10022  riotasv2d  35973  nfxnegd  41591
  Copyright terms: Public domain W3C validator