Theorem nfeq1 2907

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

Syntax hints:   = wceq 1540  Ⅎwnf 1783  Ⅎwnfc 2876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2721  df-nfc 2878

This theorem is referenced by:  euabsn  4680  invdisjrab  5082  disjxun  5093  iunopeqop  5468  fvelimad  6894  opabiotafun  6907  fvmptt  6954  eusvobj2  7345  oprabv  7413  ovmpodv2  7511  ov3  7516  dom2lem  8924  ttrcltr  9631  pwfseqlem2  10572  fsumf1o  15649  isummulc2  15688  fsum00  15724  isumshft  15765  zprod  15863  fprodf1o  15872  prodss  15873  fprodle  15922  iserodd  16766  yonedalem4b  18201  gsum2d2lem  19871  gsummptnn0fz  19884  gsummoncoe1  22212  elptr2  23478  ovoliunnul  25425  mbfinf  25583  itg2splitlem  25666  dgrle  26165  noinfbnd1  27658  disjabrex  32545  disjabrexf  32546  disjunsn  32557  voliune  34215  volfiniune  34216  bnj958  34926  bnj1491  35043  finminlem  36311  poimirlem23  37642  poimirlem28  37647  cdleme43fsv1snlem  40419  ltrniotaval  40580  cdlemksv2  40846  cdlemkuv2  40866  cdlemk36  40912  cdlemkid  40935  cdlemk19x  40942  eq0rabdioph  42769  monotoddzz  42936  disjinfi  45190  dvnprodlem1  45947  stoweidlem28  46029  stoweidlem48  46049  stoweidlem58  46059  etransclem32  46267  sge0f1o  46383  sge0gtfsumgt  46444  voliunsge0lem  46473