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

Theorem nfeqd 2754
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 2600 . 2 (𝐴 = 𝐵 ↔ ∀𝑦(𝑦𝐴𝑦𝐵))
2 nfv 1829 . . 3 𝑦𝜑
3 nfeqd.1 . . . . 5 (𝜑𝑥𝐴)
43nfcrd 2753 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐴)
5 nfeqd.2 . . . . 5 (𝜑𝑥𝐵)
65nfcrd 2753 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐵)
74, 6nfbid 1819 . . 3 (𝜑 → Ⅎ𝑥(𝑦𝐴𝑦𝐵))
82, 7nfald 2147 . 2 (𝜑 → Ⅎ𝑥𝑦(𝑦𝐴𝑦𝐵))
91, 8nfxfrd 1771 1 (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wal 1472   = wceq 1474  wnf 1698  wcel 1976  wnfc 2734
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-cleq 2599  df-nfc 2736
This theorem is referenced by:  nfeld  2755  nfeq  2758  nfned  2879  vtoclgft  3223  vtoclgftOLD  3224  sbcralt  3473  csbiebt  3515  dfnfc2  4381  dfnfc2OLD  4382  eusvnfb  4780  eusv2i  4781  dfid3  4941  nfiotad  5754  iota2df  5775  riota5f  6510  oprabid  6551  axrepndlem1  9267  axrepndlem2  9268  axunnd  9271  axpowndlem4  9275  axregndlem2  9278  axinfndlem1  9280  axinfnd  9281  axacndlem4  9285  axacndlem5  9286  axacnd  9287  riotasv2d  33061  riotaeqimp  40162
  Copyright terms: Public domain W3C validator