Theorem nfeq1 2918

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

Syntax hints:   = wceq 1536  Ⅎwnf 1779  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780  df-cleq 2726  df-nfc 2889

This theorem is referenced by:  euabsn  4730  invdisjrab  5134  disjxun  5145  iunopeqop  5530  fvelimad  6975  opabiotafun  6988  fvmptt  7035  eusvobj2  7422  oprabv  7492  ovmpodv2  7590  ov3  7595  dom2lem  9030  ttrcltr  9753  pwfseqlem2  10696  fsumf1o  15755  isummulc2  15794  fsum00  15830  isumshft  15871  zprod  15969  fprodf1o  15978  prodss  15979  fprodle  16028  iserodd  16868  yonedalem4b  18332  gsum2d2lem  20005  gsummptnn0fz  20018  gsummoncoe1  22327  elptr2  23597  ovoliunnul  25555  mbfinf  25713  itg2splitlem  25797  dgrle  26296  noinfbnd1  27788  disjabrex  32601  disjabrexf  32602  disjunsn  32613  voliune  34209  volfiniune  34210  bnj958  34932  bnj1491  35049  finminlem  36300  poimirlem23  37629  poimirlem28  37634  cdleme43fsv1snlem  40402  ltrniotaval  40563  cdlemksv2  40829  cdlemkuv2  40849  cdlemk36  40895  cdlemkid  40918  cdlemk19x  40925  eq0rabdioph  42763  monotoddzz  42931  disjinfi  45134  dvnprodlem1  45901  stoweidlem28  45983  stoweidlem48  46003  stoweidlem58  46013  etransclem32  46221  sge0f1o  46337  sge0gtfsumgt  46398  voliunsge0lem  46427