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

Theorem nfeqd 2619
 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 2465 . 2
2 nfv 1769 . . 3
3 nfeqd.1 . . . . 5
43nfcrd 2618 . . . 4
5 nfeqd.2 . . . . 5
65nfcrd 2618 . . . 4
74, 6nfbid 2036 . . 3
82, 7nfald 2053 . 2
91, 8nfxfrd 1705 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189  wal 1450   wceq 1452  wnf 1675   wcel 1904  wnfc 2599 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-ext 2451 This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676  df-cleq 2464  df-nfc 2601 This theorem is referenced by:  nfeld  2620  nfeq  2623  nfned  2743  vtoclgft  3082  sbcralt  3328  csbiebt  3369  dfnfc2  4208  eusvnfb  4597  eusv2i  4598  dfid3  4755  nfiotad  5556  iota2df  5577  riota5f  6294  oprabid  6335  axrepndlem1  9035  axrepndlem2  9036  axunnd  9039  axpowndlem4  9043  axregndlem2  9046  axinfndlem1  9048  axinfnd  9049  axacndlem4  9053  axacndlem5  9054  axacnd  9055  riotasv2d  32593  riotaeqimp  39183
 Copyright terms: Public domain W3C validator