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 ⊢ Ⅎ𝑥 𝐴 = 𝐵

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

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 2753  df-nfc 2910

This theorem is used by:  euabsn  4687  invdisjrab  5090  disjxun  5101  iunopeqop  5494  iunopeqopOLD  5495  fvelimad  6950  opabiotafun  6963  fvmptt  7012  eusvobj2  7410  oprabv  7478  ovmpodv2  7576  ov3  7581  dom2lem  9012  ttrcltr  9710  pwfseqlem2  10737  fsumf1o  15882  isummulc2  15921  fsum00  15958  isumshft  16001  zprod  16097  fprodf1o  16106  prodss  16107  fprodle  16156  iserodd  17006  yonedalem4b  18443  gsum2d2lem  20180  gsummptnn0fz  20193  gsummoncoe1  22619  elptr2  23886  ovoliunnul  25821  mbfinf  25979  itg2splitlem  26062  dgrle  26555  noinfbnd1  28079  disjabrex  33169  disjabrexf  33170  disjunsn  33181  voliune  34855  volfiniune  34856  bnj958  35563  bnj1491  35680  finminlem  37086  poimirlem23  38541  poimirlem28  38546  cdleme43fsv1snlem  41457  ltrniotaval  41618  cdlemksv2  41884  cdlemkuv2  41904  cdlemk36  41950  cdlemkid  41973  cdlemk19x  41980  eq0rabdioph  43766  monotoddzz  43929  disjinfi  46176  dvnprodlem1  46925  stoweidlem28  47007  stoweidlem48  47027  stoweidlem58  47037  etransclem32  47245  sge0f1o  47361  sge0gtfsumgt  47422  voliunsge0lem  47451  sssmf  47717