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.

Step	Hyp	Ref	Expression
1		dfcleq 2450	. 2
2		nfv 1707	. . 3
3		nfeqd.1	. . . . 5
4	3	nfcrd 2625	. . . 4
5		nfeqd.2	. . . . 5
6	5	nfcrd 2625	. . . 4
7	4, 6	nfbid 1933	. . 3
8	2, 7	nfald 1951	. 2
9	1, 8	nfxfrd 1646	1

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