Theorem nfeq1 2938

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

Syntax hints:   = wceq 1559  Ⅎwnf 1802  Ⅎwnfc 2908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-nf 1803  df-cleq 2753  df-nfc 2910

This theorem is referenced by:  euabsn  4682  invdisjrab  5084  disjxun  5095  iunopeqop  5487  iunopeqopOLD  5488  fvelimad  6929  opabiotafun  6942  fvmptt  6991  eusvobj2  7383  oprabv  7451  ovmpodv2  7549  ov3  7554  dom2lem  8967  ttrcltr  9665  pwfseqlem2  10611  fsumf1o  15741  isummulc2  15780  fsum00  15817  isumshft  15860  zprod  15958  fprodf1o  15967  prodss  15968  fprodle  16017  iserodd  16862  yonedalem4b  18299  gsum2d2lem  20004  gsummptnn0fz  20017  gsummoncoe1  22359  elptr2  23622  ovoliunnul  25557  mbfinf  25715  itg2splitlem  25798  dgrle  26291  noinfbnd1  27781  disjabrex  32742  disjabrexf  32743  disjunsn  32754  voliune  34487  volfiniune  34488  bnj958  35196  bnj1491  35313  finminlem  36639  poimirlem23  38103  poimirlem28  38108  cdleme43fsv1snlem  41005  ltrniotaval  41166  cdlemksv2  41432  cdlemkuv2  41452  cdlemk36  41498  cdlemkid  41521  cdlemk19x  41528  eq0rabdioph  43318  monotoddzz  43481  disjinfi  45731  dvnprodlem1  46481  stoweidlem28  46563  stoweidlem48  46583  stoweidlem58  46593  etransclem32  46801  sge0f1o  46917  sge0gtfsumgt  46978  voliunsge0lem  47007  sssmf  47273