Theorem nfeq1 2922

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

Syntax hints:   = wceq 1539  Ⅎwnf 1786  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-cleq 2730  df-nfc 2889

This theorem is referenced by:  euabsn  4662  invdisjrabw  5059  invdisjrab  5060  disjxun  5072  iunopeqop  5435  fvelimad  6836  opabiotafun  6849  fvmptt  6895  eusvobj2  7268  oprabv  7335  ovmpodv2  7431  ov3  7435  dom2lem  8780  ttrcltr  9474  pwfseqlem2  10415  fsumf1o  15435  isummulc2  15474  fsum00  15510  isumshft  15551  zprod  15647  fprodf1o  15656  prodss  15657  fprodle  15706  iserodd  16536  yonedalem4b  17994  gsum2d2lem  19574  gsummptnn0fz  19587  gsummoncoe1  21475  elptr2  22725  ovoliunnul  24671  mbfinf  24829  itg2splitlem  24913  dgrle  25404  disjabrex  30921  disjabrexf  30922  disjunsn  30933  voliune  32197  volfiniune  32198  bnj958  32920  bnj1491  33037  noinfbnd1  33932  finminlem  34507  poimirlem23  35800  poimirlem28  35805  cdleme43fsv1snlem  38434  ltrniotaval  38595  cdlemksv2  38861  cdlemkuv2  38881  cdlemk36  38927  cdlemkid  38950  cdlemk19x  38957  eq0rabdioph  40598  monotoddzz  40765  disjinfi  42731  stoweidlem28  43569  stoweidlem48  43589  stoweidlem58  43599  etransclem32  43807  sge0gtfsumgt  43981  voliunsge0lem  44010