Theorem nfeq 2940

Description: Hypothesis builder for equality. (Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)

Hypotheses

Ref	Expression
nfnfc.1	⊢ Ⅎ𝑥𝐴
nfeq.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfeq	⊢ Ⅎ𝑥 𝐴 = 𝐵

Proof of Theorem nfeq

Step	Hyp	Ref	Expression
1		nfnfc.1	. . . 4 ⊢ Ⅎ𝑥𝐴
2	1	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
3		nfeq.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	3	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐵)
5	2, 4	nfeqd 2937	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴 = 𝐵)
6	5	mptru 1577	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

This proof depends on syntax axioms:   = wceq 1570  ⊤wtru 1571  Ⅎ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:  nfeq1  2942  nfeq2  2944  nfne  3063  raleqf  3347  rmoeq1f  3408  rabeqf  3452  csbhypf  3882  sbceqg  4377  nffn  6638  nffo  6795  fvmptd3f  7009  mpteqb  7013  fvmptf  7015  eqfnfv2f  7033  dff13f  7258  ovmpos  7567  ov2gf  7568  ovmpodxf  7569  ovmpodf  7575  eqerlem  8736  seqof2  14114  sumeq2ii  15768  sumss  15798  fsumadd  15814  fsummulc2  15858  fsumrelem  15882  prodeq1f  15983  prodeq2ii  15988  fprodmul  16037  fproddiv  16038  txcnp  23828  ptcnplem  23829  cnmpt11  23871  cnmpt21  23879  cnmptcom  23886  mbfeqalem1  25851  mbflim  25878  itgeq1f  25981  itgeq1fOLD  25982  itgeqa  26024  dvmptfsum  26185  ulmss  26611  leibpi  27158  o1cxp  27190  lgseisenlem2  27591  nosupbnd1  27929  2ndresdju  33065  aciunf1lem  33078  deg1prod  33937  sigapildsys  34617  bnj1316  35273  bnj1446  35498  bnj1447  35499  bnj1448  35500  bnj1519  35518  bnj1520  35519  bnj1529  35523  subtr  36882  subtr2  36883  bj-sbeqALT  37592  poimirlem25  38353  iuneq2f  38863  mpobi123f  38869  mptbi12f  38873  dvdsrabdioph  43595  fphpd  43601  mnringmulrcld  45010  fvelrnbf  45796  refsum2cnlem1  45815  elrnmpt1sf  45965  choicefi  45975  axccdom  45996  uzublem  46202  fsumf1of  46348  fmuldfeq  46357  mccl  46372  climmulf  46378  climexp  46379  climsuse  46382  climrecf  46383  climaddf  46389  mullimc  46390  neglimc  46419  addlimc  46420  0ellimcdiv  46421  climeldmeqmpt  46440  climfveqmpt  46443  climfveqf  46452  climfveqmpt3  46454  climeldmeqf  46455  climeqf  46460  climeldmeqmpt3  46461  limsupubuzlem  46484  limsupequz  46495  dvnmptdivc  46710  dvmptfprod  46717  stoweidlem18  46790  stoweidlem31  46803  stoweidlem55  46827  stoweidlem59  46831  sge0iunmpt  47190  sge0reuz  47219  iundjiun  47232  hoicvrrex  47328  ovnhoilem1  47373  ovnlecvr2  47382  opnvonmbllem1  47404  vonioo  47454  vonicc  47457  smflim  47549  smfpimcclem  47579  smfpimcc  47580  cfsetsnfsetf  47853  ovmpordxf  49176