Theorem nfeq1 2955

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

Syntax hints:   = wceq 1653  Ⅎwnf 1879  Ⅎwnfc 2928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-cleq 2792  df-nfc 2930

This theorem is referenced by:  euabsn  4450  invdisjrab  4830  disjxun  4841  iunopeqop  5177  opabiotafun  6484  fvmptt  6525  eusvobj2  6871  oprabv  6937  ovmpt2dv2  7028  ov3  7031  dom2lem  8235  pwfseqlem2  9769  fsumf1o  14795  isummulc2  14832  fsum00  14868  isumshft  14909  zprod  15004  fprodf1o  15013  prodss  15014  iserodd  15873  yonedalem4b  17231  gsum2d2lem  18687  gsummptnn0fz  18697  gsummptnn0fzOLD  18698  gsummoncoe1  19996  elptr2  21706  ovoliunnul  23615  mbfinf  23773  itg2splitlem  23856  dgrle  24340  disjabrex  29912  disjabrexf  29913  disjunsn  29924  voliune  30808  volfiniune  30809  bnj958  31527  bnj1491  31642  finminlem  32825  poimirlem23  33921  poimirlem28  33926  cdleme43fsv1snlem  36441  ltrniotaval  36602  cdlemksv2  36868  cdlemkuv2  36888  cdlemk36  36934  cdlemkid  36957  cdlemk19x  36964  eq0rabdioph  38126  monotoddzz  38293  cncfiooicclem1  40850  stoweidlem28  40988  stoweidlem48  41008  stoweidlem58  41018  etransclem32  41226  sge0gtfsumgt  41403  voliunsge0lem  41432