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

Theorem nfeqd 2623
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 2447 . 2
2 nfv 1674 . . 3
3 nfeqd.1 . . . . 5
43nfcrd 2622 . . . 4
5 nfeqd.2 . . . . 5
65nfcrd 2622 . . . 4
74, 6nfbid 1871 . . 3
82, 7nfald 1889 . 2
91, 8nfxfrd 1617 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  A.wal 1368  =wceq 1370  F/wnf 1590  e.wcel 1758  F/_wnfc 2602
This theorem is referenced by:  nfeld  2624  nfeq  2627  nfned  2785  vtoclgft  3129  sbcralt  3378  csbiebt  3421  dfnfc2  4226  eusvnfb  4605  eusv2i  4606  dfid3  4754  nfiotad  5503  iota2df  5524  riota5f  6208  oprabid  6246  axrepndlem1  8893  axrepndlem2  8894  axunnd  8897  axpowndlem2OLD  8900  axpowndlem4  8903  axregndlem2  8906  axinfndlem1  8909  axinfnd  8910  axacndlem4  8914  axacndlem5  8915  axacnd  8916  riotasv2d  33459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-cleq 2446  df-nfc 2604
  Copyright terms: Public domain W3C validator