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  4671  invdisjrab  5073  disjxun  5084  iunopeqop  5469  fvelimad  6901  opabiotafun  6914  fvmptt  6962  eusvobj2  7352  oprabv  7420  ovmpodv2  7518  ov3  7523  dom2lem  8932  ttrcltr  9628  pwfseqlem2  10573  fsumf1o  15676  isummulc2  15715  fsum00  15752  isumshft  15795  zprod  15893  fprodf1o  15902  prodss  15903  fprodle  15952  iserodd  16797  yonedalem4b  18233  gsum2d2lem  19939  gsummptnn0fz  19952  gsummoncoe1  22283  elptr2  23549  ovoliunnul  25484  mbfinf  25642  itg2splitlem  25725  dgrle  26218  noinfbnd1  27707  disjabrex  32667  disjabrexf  32668  disjunsn  32679  voliune  34389  volfiniune  34390  bnj958  35098  bnj1491  35215  finminlem  36516  poimirlem23  37978  poimirlem28  37983  cdleme43fsv1snlem  40880  ltrniotaval  41041  cdlemksv2  41307  cdlemkuv2  41327  cdlemk36  41373  cdlemkid  41396  cdlemk19x  41403  eq0rabdioph  43222  monotoddzz  43389  disjinfi  45640  dvnprodlem1  46392  stoweidlem28  46474  stoweidlem48  46494  stoweidlem58  46504  etransclem32  46712  sge0f1o  46828  sge0gtfsumgt  46889  voliunsge0lem  46918