Theorem nfeq1 2919

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

Syntax hints:   = wceq 1543  Ⅎwnf 1791  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-cleq 2729  df-nfc 2886

This theorem is referenced by:  euabsn  4642  invdisjrabw  5038  invdisjrab  5039  disjxun  5051  iunopeqop  5404  fvelimad  6779  opabiotafun  6792  fvmptt  6838  eusvobj2  7206  oprabv  7271  ovmpodv2  7367  ov3  7371  dom2lem  8668  pwfseqlem2  10273  fsumf1o  15287  isummulc2  15326  fsum00  15362  isumshft  15403  zprod  15499  fprodf1o  15508  prodss  15509  fprodle  15558  iserodd  16388  yonedalem4b  17784  gsum2d2lem  19358  gsummptnn0fz  19371  gsummoncoe1  21225  elptr2  22471  ovoliunnul  24404  mbfinf  24562  itg2splitlem  24646  dgrle  25137  disjabrex  30640  disjabrexf  30641  disjunsn  30652  voliune  31909  volfiniune  31910  bnj958  32633  bnj1491  32750  ttrcltr  33515  noinfbnd1  33669  finminlem  34244  poimirlem23  35537  poimirlem28  35542  cdleme43fsv1snlem  38171  ltrniotaval  38332  cdlemksv2  38598  cdlemkuv2  38618  cdlemk36  38664  cdlemkid  38687  cdlemk19x  38694  eq0rabdioph  40301  monotoddzz  40468  disjinfi  42404  stoweidlem28  43244  stoweidlem48  43264  stoweidlem58  43274  etransclem32  43482  sge0gtfsumgt  43656  voliunsge0lem  43685