Theorem nfeq1 2942

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

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

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 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

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 2757  df-nfc 2914

This theorem is used by:  euabsn  4694  invdisjrab  5098  disjxun  5109  iunopeqop  5506  iunopeqopOLD  5507  fvelimad  6952  opabiotafun  6965  fvmptt  7014  eusvobj2  7408  oprabv  7476  ovmpodv2  7574  ov3  7579  dom2lem  8991  ttrcltr  9688  pwfseqlem2  10655  fsumf1o  15793  isummulc2  15832  fsum00  15869  isumshft  15912  zprod  16010  fprodf1o  16019  prodss  16020  fprodle  16069  iserodd  16913  yonedalem4b  18350  gsum2d2lem  20067  gsummptnn0fz  20080  gsummoncoe1  22498  elptr2  23762  ovoliunnul  25697  mbfinf  25855  itg2splitlem  25938  dgrle  26431  noinfbnd1  27924  disjabrex  32974  disjabrexf  32975  disjunsn  32986  voliune  34660  volfiniune  34661  bnj958  35369  bnj1491  35486  finminlem  36862  poimirlem23  38327  poimirlem28  38332  cdleme43fsv1snlem  41227  ltrniotaval  41388  cdlemksv2  41654  cdlemkuv2  41674  cdlemk36  41720  cdlemkid  41743  cdlemk19x  41750  eq0rabdioph  43540  monotoddzz  43703  disjinfi  45943  dvnprodlem1  46693  stoweidlem28  46775  stoweidlem48  46795  stoweidlem58  46805  etransclem32  47013  sge0f1o  47129  sge0gtfsumgt  47190  voliunsge0lem  47219  sssmf  47485