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 1540  Ⅎwnf 1783  Ⅎwnfc 2883

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 2007  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

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 2727  df-nfc 2885

This theorem is referenced by:  euabsn  4702  invdisjrab  5106  disjxun  5117  iunopeqop  5496  fvelimad  6946  opabiotafun  6959  fvmptt  7006  eusvobj2  7397  oprabv  7467  ovmpodv2  7565  ov3  7570  dom2lem  9006  ttrcltr  9730  pwfseqlem2  10673  fsumf1o  15739  isummulc2  15778  fsum00  15814  isumshft  15855  zprod  15953  fprodf1o  15962  prodss  15963  fprodle  16012  iserodd  16855  yonedalem4b  18288  gsum2d2lem  19954  gsummptnn0fz  19967  gsummoncoe1  22246  elptr2  23512  ovoliunnul  25460  mbfinf  25618  itg2splitlem  25701  dgrle  26200  noinfbnd1  27693  disjabrex  32563  disjabrexf  32564  disjunsn  32575  voliune  34260  volfiniune  34261  bnj958  34971  bnj1491  35088  finminlem  36336  poimirlem23  37667  poimirlem28  37672  cdleme43fsv1snlem  40439  ltrniotaval  40600  cdlemksv2  40866  cdlemkuv2  40886  cdlemk36  40932  cdlemkid  40955  cdlemk19x  40962  eq0rabdioph  42799  monotoddzz  42967  disjinfi  45216  dvnprodlem1  45975  stoweidlem28  46057  stoweidlem48  46077  stoweidlem58  46087  etransclem32  46295  sge0f1o  46411  sge0gtfsumgt  46472  voliunsge0lem  46501