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 1542  Ⅎwnf 1785  Ⅎwnfc 2883

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 2708

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

This theorem is referenced by:  euabsn  4670  invdisjrab  5072  disjxun  5083  iunopeqop  5475  iunopeqopOLD  5476  fvelimad  6907  opabiotafun  6920  fvmptt  6968  eusvobj2  7359  oprabv  7427  ovmpodv2  7525  ov3  7530  dom2lem  8939  ttrcltr  9637  pwfseqlem2  10582  fsumf1o  15685  isummulc2  15724  fsum00  15761  isumshft  15804  zprod  15902  fprodf1o  15911  prodss  15912  fprodle  15961  iserodd  16806  yonedalem4b  18242  gsum2d2lem  19948  gsummptnn0fz  19961  gsummoncoe1  22273  elptr2  23539  ovoliunnul  25474  mbfinf  25632  itg2splitlem  25715  dgrle  26208  noinfbnd1  27693  disjabrex  32652  disjabrexf  32653  disjunsn  32664  voliune  34373  volfiniune  34374  bnj958  35082  bnj1491  35199  finminlem  36500  poimirlem23  37964  poimirlem28  37969  cdleme43fsv1snlem  40866  ltrniotaval  41027  cdlemksv2  41293  cdlemkuv2  41313  cdlemk36  41359  cdlemkid  41382  cdlemk19x  41389  eq0rabdioph  43208  monotoddzz  43371  disjinfi  45622  dvnprodlem1  46374  stoweidlem28  46456  stoweidlem48  46476  stoweidlem58  46486  etransclem32  46694  sge0f1o  46810  sge0gtfsumgt  46871  voliunsge0lem  46900