Theorem nfeq1 2908

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

Syntax hints:   = wceq 1540  Ⅎwnf 1783  Ⅎwnfc 2877

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 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

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 2722  df-nfc 2879

This theorem is referenced by:  euabsn  4692  invdisjrab  5096  disjxun  5107  iunopeqop  5483  fvelimad  6930  opabiotafun  6943  fvmptt  6990  eusvobj2  7381  oprabv  7451  ovmpodv2  7549  ov3  7554  dom2lem  8965  ttrcltr  9675  pwfseqlem2  10618  fsumf1o  15695  isummulc2  15734  fsum00  15770  isumshft  15811  zprod  15909  fprodf1o  15918  prodss  15919  fprodle  15968  iserodd  16812  yonedalem4b  18243  gsum2d2lem  19909  gsummptnn0fz  19922  gsummoncoe1  22201  elptr2  23467  ovoliunnul  25414  mbfinf  25572  itg2splitlem  25655  dgrle  26154  noinfbnd1  27647  disjabrex  32517  disjabrexf  32518  disjunsn  32529  voliune  34225  volfiniune  34226  bnj958  34936  bnj1491  35053  finminlem  36301  poimirlem23  37632  poimirlem28  37637  cdleme43fsv1snlem  40409  ltrniotaval  40570  cdlemksv2  40836  cdlemkuv2  40856  cdlemk36  40902  cdlemkid  40925  cdlemk19x  40932  eq0rabdioph  42757  monotoddzz  42925  disjinfi  45179  dvnprodlem1  45937  stoweidlem28  46019  stoweidlem48  46039  stoweidlem58  46049  etransclem32  46257  sge0f1o  46373  sge0gtfsumgt  46434  voliunsge0lem  46463