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

Theorem nfeqd 2626
 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 2450 . 2
2 nfv 1707 . . 3
3 nfeqd.1 . . . . 5
43nfcrd 2625 . . . 4
5 nfeqd.2 . . . . 5
65nfcrd 2625 . . . 4
74, 6nfbid 1933 . . 3
82, 7nfald 1951 . 2
91, 8nfxfrd 1646 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  =wceq 1395  F/wnf 1616  e.wcel 1818  F/_wnfc 2605 This theorem is referenced by:  nfeld  2627  nfeq  2630  nfned  2789  vtoclgft  3157  sbcralt  3408  csbiebt  3454  dfnfc2  4267  eusvnfb  4648  eusv2i  4649  dfid3  4801  nfiotad  5559  iota2df  5580  riota5f  6282  oprabid  6323  axrepndlem1  8988  axrepndlem2  8989  axunnd  8992  axpowndlem2OLD  8995  axpowndlem4  8998  axregndlem2  9001  axinfndlem1  9004  axinfnd  9005  axacndlem4  9009  axacndlem5  9010  axacnd  9011  riotasv2d  34688 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-cleq 2449  df-nfc 2607
 Copyright terms: Public domain W3C validator