Theorem nfeq1 2915

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 2899	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfeq 2913	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-cleq 2729  df-nfc 2886

This theorem is referenced by:  euabsn  4685  invdisjrab  5087  disjxun  5098  iunopeqop  5477  fvelimad  6909  opabiotafun  6922  fvmptt  6970  eusvobj2  7360  oprabv  7428  ovmpodv2  7526  ov3  7531  dom2lem  8941  ttrcltr  9637  pwfseqlem2  10582  fsumf1o  15658  isummulc2  15697  fsum00  15733  isumshft  15774  zprod  15872  fprodf1o  15881  prodss  15882  fprodle  15931  iserodd  16775  yonedalem4b  18211  gsum2d2lem  19914  gsummptnn0fz  19927  gsummoncoe1  22264  elptr2  23530  ovoliunnul  25476  mbfinf  25634  itg2splitlem  25717  dgrle  26216  noinfbnd1  27709  disjabrex  32668  disjabrexf  32669  disjunsn  32680  voliune  34406  volfiniune  34407  bnj958  35115  bnj1491  35232  finminlem  36531  poimirlem23  37891  poimirlem28  37896  cdleme43fsv1snlem  40793  ltrniotaval  40954  cdlemksv2  41220  cdlemkuv2  41240  cdlemk36  41286  cdlemkid  41309  cdlemk19x  41316  eq0rabdioph  43130  monotoddzz  43297  disjinfi  45548  dvnprodlem1  46301  stoweidlem28  46383  stoweidlem48  46403  stoweidlem58  46413  etransclem32  46621  sge0f1o  46737  sge0gtfsumgt  46798  voliunsge0lem  46827