Theorem nfeq1 2919

Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)

Hypothesis

Ref	Expression
nfeq1.1	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
nfeq1	⊢ Ⅎ𝑥 𝐴 = 𝐵

Distinct variable group:   𝑥,𝐵

Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem nfeq1

Step	Hyp	Ref	Expression
1		nfeq1.1	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2904	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfeq 2917	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1542  Ⅎwnf 1786  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-cleq 2725  df-nfc 2886

This theorem is referenced by:  euabsn  4731  invdisjrabw  5134  invdisjrab  5135  disjxun  5147  iunopeqop  5522  fvelimad  6960  opabiotafun  6973  fvmptt  7019  eusvobj2  7401  oprabv  7469  ovmpodv2  7566  ov3  7570  dom2lem  8988  ttrcltr  9711  pwfseqlem2  10654  fsumf1o  15669  isummulc2  15708  fsum00  15744  isumshft  15785  zprod  15881  fprodf1o  15890  prodss  15891  fprodle  15940  iserodd  16768  yonedalem4b  18229  gsum2d2lem  19841  gsummptnn0fz  19854  gsummoncoe1  21828  elptr2  23078  ovoliunnul  25024  mbfinf  25182  itg2splitlem  25266  dgrle  25757  noinfbnd1  27232  disjabrex  31813  disjabrexf  31814  disjunsn  31825  voliune  33227  volfiniune  33228  bnj958  33951  bnj1491  34068  finminlem  35203  poimirlem23  36511  poimirlem28  36516  cdleme43fsv1snlem  39291  ltrniotaval  39452  cdlemksv2  39718  cdlemkuv2  39738  cdlemk36  39784  cdlemkid  39807  cdlemk19x  39814  eq0rabdioph  41514  monotoddzz  41682  disjinfi  43891  stoweidlem28  44744  stoweidlem48  44764  stoweidlem58  44774  etransclem32  44982  sge0gtfsumgt  45159  voliunsge0lem  45188