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

Theorem nfeqd 2586
 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 2430 . 2
2 nfv 1629 . . 3
3 nfeqd.1 . . . . 5
43nfcrd 2585 . . . 4
5 nfeqd.2 . . . . 5
65nfcrd 2585 . . . 4
74, 6nfbid 1854 . . 3
82, 7nfald 1871 . 2
91, 8nfxfrd 1580 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177  wal 1549  wnf 1553   wceq 1652   wcel 1725  wnfc 2559 This theorem is referenced by:  nfeld  2587  nfned  2696  vtoclgft  3002  sbcralt  3233  csbiebt  3287  dfnfc2  4033  dfid3  4499  eusvnfb  4719  eusv2i  4720  nfiotad  5421  iota2df  5442  oprabid  6105  riota5f  6574  riotasvdOLD  6593  riotasv2d  6594  riotasv2dOLD  6595  axrepndlem1  8467  axrepndlem2  8468  axunnd  8471  axpowndlem2  8473  axpowndlem4  8475  axregndlem2  8478  axinfndlem1  8480  axinfnd  8481  axacndlem4  8485  axacndlem5  8486  axacnd  8487 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-ext 2417 This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-cleq 2429  df-nfc 2561
 Copyright terms: Public domain W3C validator