Theorem nfeq1 2807

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

Syntax hints:   = wceq 1523  Ⅎwnf 1748  Ⅎwnfc 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-cleq 2644  df-nfc 2782

This theorem is referenced by:  euabsn  4293  invdisjrab  4671  disjxun  4683  iunopeqop  5010  opabiotafun  6298  fvmptt  6339  eusvobj2  6683  oprabv  6745  ovmpt2dv2  6836  ov3  6839  dom2lem  8037  pwfseqlem2  9519  fsumf1o  14498  isummulc2  14537  fsum00  14574  isumshft  14615  zprod  14711  fprodf1o  14720  prodss  14721  iserodd  15587  yonedalem4b  16963  gsum2d2lem  18418  gsummptnn0fz  18428  gsummoncoe1  19722  elptr2  21425  ovoliunnul  23321  mbfinf  23477  itg2splitlem  23560  dgrle  24044  disjabrex  29521  disjabrexf  29522  disjunsn  29533  voliune  30420  volfiniune  30421  bnj958  31136  bnj1491  31251  finminlem  32437  poimirlem23  33562  poimirlem28  33567  cdleme43fsv1snlem  36025  ltrniotaval  36186  cdlemksv2  36452  cdlemkuv2  36472  cdlemk36  36518  cdlemkid  36541  cdlemk19x  36548  eq0rabdioph  37657  monotoddzz  37825  cncfiooicclem1  40424  stoweidlem28  40563  stoweidlem48  40583  stoweidlem58  40593  etransclem32  40801  sge0gtfsumgt  40978  voliunsge0lem  41007