Theorem nfeq1 2941

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

This proof depends on syntax axioms:   = wceq 1570  Ⅎwnf 1816  Ⅎwnfc 2911

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-cleq 2755  df-nfc 2913

This theorem is used by:  euabsn  4689  invdisjrab  5095  disjxun  5106  iunopeqop  5501  iunopeqopOLD  5502  fvelimad  6983  opabiotafun  6996  fvmptt  7045  eusvobj2  7443  oprabv  7511  ovmpodv2  7610  ov3  7615  dom2lem  9057  ttrcltr  9754  pwfseqlem2  10783  fsumf1o  15933  isummulc2  15972  fsum00  16009  isumshft  16052  zprod  16148  fprodf1o  16157  prodss  16158  fprodle  16207  iserodd  17057  yonedalem4b  18500  gsum2d2lem  20238  gsummptnn0fz  20251  gsummoncoe1  22681  elptr2  23948  ovoliunnul  25883  mbfinf  26041  itg2splitlem  26124  dgrle  26617  noinfbnd1  28143  disjabrex  33274  disjabrexf  33275  disjunsn  33286  voliune  34973  volfiniune  34974  bnj958  35681  bnj1491  35798  srepdflem1  36126  finminlem  37321  poimirlem23  38829  poimirlem28  38834  cdleme43fsv1snlem  41743  ltrniotaval  41904  cdlemksv2  42170  cdlemkuv2  42190  cdlemk36  42236  cdlemkid  42259  cdlemk19x  42266  eq0rabdioph  44053  monotoddzz  44216  disjinfi  46480  dvnprodlem1  47229  stoweidlem28  47311  stoweidlem48  47331  stoweidlem58  47341  etransclem32  47549  sge0f1o  47665  sge0gtfsumgt  47726  voliunsge0lem  47755  sssmf  48021