Theorem nfeq 2936

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 2933	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴 = 𝐵)
6	5	mptru 1577	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

This proof depends on syntax axioms:   = wceq 1570  ⊤wtru 1571  Ⅎ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:  nfeq1  2938  nfeq2  2940  nfne  3059  raleqf  3342  rmoeq1f  3403  rabeqf  3446  csbhypf  3875  sbceqg  4370  nffn  6636  nffo  6793  fvmptd3f  7007  mpteqb  7011  fvmptf  7013  eqfnfv2f  7031  dff13f  7257  ovmpos  7566  ov2gf  7567  ovmpodxf  7568  ovmpodf  7574  eqerlem  8746  seqof2  14196  sumeq2ii  15853  sumss  15883  fsumadd  15899  fsummulc2  15943  fsumrelem  15967  prodeq1f  16068  prodeq2ii  16073  fprodmul  16120  fproddiv  16121  txcnp  23932  ptcnplem  23933  cnmpt11  23975  cnmpt21  23983  cnmptcom  23990  mbfeqalem1  25955  mbflim  25982  itgeq1f  26085  itgeqa  26127  dvmptfsum  26288  ulmss  26717  leibpi  27263  o1cxp  27295  lgseisenlem2  27696  nosupbnd1  28064  2ndresdju  33236  aciunf1lem  33249  deg1prod  34108  sigapildsys  34788  bnj1316  35443  bnj1446  35668  bnj1447  35669  bnj1448  35670  bnj1519  35688  bnj1520  35689  bnj1529  35693  subtr  37082  subtr2  37083  bj-sbeqALT  37792  poimirlem25  38543  iuneq2f  39068  mpobi123f  39074  mptbi12f  39078  dvdsrabdioph  43796  fphpd  43802  mnringmulrcld  45211  fvelrnbf  46004  refsum2cnlem1  46023  elrnmpt1sf  46173  choicefi  46183  axccdom  46204  uzublem  46409  fsumf1of  46555  fmuldfeq  46564  mccl  46579  climmulf  46585  climexp  46586  climsuse  46589  climrecf  46590  climaddf  46596  mullimc  46597  neglimc  46626  addlimc  46627  0ellimcdiv  46628  climeldmeqmpt  46647  climfveqmpt  46650  climfveqf  46659  climfveqmpt3  46661  climeldmeqf  46662  climeqf  46667  climeldmeqmpt3  46668  limsupubuzlem  46691  limsupequz  46702  dvnmptdivc  46917  dvmptfprod  46924  stoweidlem18  46997  stoweidlem31  47010  stoweidlem55  47034  stoweidlem59  47038  sge0iunmpt  47397  sge0reuz  47426  iundjiun  47439  hoicvrrex  47535  ovnhoilem1  47580  ovnlecvr2  47589  opnvonmbllem1  47611  vonioo  47661  vonicc  47664  smflim  47756  smfpimcclem  47786  smfpimcc  47787  cfsetsnfsetf  48097  ovmpordxf  49420