Theorem nfeq1 2914

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

Syntax hints:   = wceq 1541  Ⅎwnf 1784  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2728  df-nfc 2885

This theorem is referenced by:  euabsn  4683  invdisjrab  5085  disjxun  5096  iunopeqop  5469  fvelimad  6901  opabiotafun  6914  fvmptt  6961  eusvobj2  7350  oprabv  7418  ovmpodv2  7516  ov3  7521  dom2lem  8929  ttrcltr  9625  pwfseqlem2  10570  fsumf1o  15646  isummulc2  15685  fsum00  15721  isumshft  15762  zprod  15860  fprodf1o  15869  prodss  15870  fprodle  15919  iserodd  16763  yonedalem4b  18199  gsum2d2lem  19902  gsummptnn0fz  19915  gsummoncoe1  22252  elptr2  23518  ovoliunnul  25464  mbfinf  25622  itg2splitlem  25705  dgrle  26204  noinfbnd1  27697  disjabrex  32657  disjabrexf  32658  disjunsn  32669  voliune  34386  volfiniune  34387  bnj958  35096  bnj1491  35213  finminlem  36512  poimirlem23  37844  poimirlem28  37849  cdleme43fsv1snlem  40680  ltrniotaval  40841  cdlemksv2  41107  cdlemkuv2  41127  cdlemk36  41173  cdlemkid  41196  cdlemk19x  41203  eq0rabdioph  43018  monotoddzz  43185  disjinfi  45436  dvnprodlem1  46190  stoweidlem28  46272  stoweidlem48  46292  stoweidlem58  46302  etransclem32  46510  sge0f1o  46626  sge0gtfsumgt  46687  voliunsge0lem  46716