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  6638  nffo  6795  fvmptd3f  7009  mpteqb  7013  fvmptf  7015  eqfnfv2f  7033  dff13f  7259  ovmpos  7568  ov2gf  7569  ovmpodxf  7570  ovmpodf  7576  eqerlem  8753  seqof2  14203  sumeq2ii  15860  sumss  15890  fsumadd  15906  fsummulc2  15950  fsumrelem  15974  prodeq1f  16075  prodeq2ii  16080  fprodmul  16127  fproddiv  16128  txcnp  23939  ptcnplem  23940  cnmpt11  23982  cnmpt21  23990  cnmptcom  23997  mbfeqalem1  25962  mbflim  25989  itgeq1f  26092  itgeqa  26134  dvmptfsum  26295  ulmss  26724  leibpi  27270  o1cxp  27302  lgseisenlem2  27703  nosupbnd1  28071  2ndresdju  33243  aciunf1lem  33256  deg1prod  34115  sigapildsys  34795  bnj1316  35450  bnj1446  35675  bnj1447  35676  bnj1448  35677  bnj1519  35695  bnj1520  35696  bnj1529  35700  subtr  37102  subtr2  37103  bj-sbeqALT  37812  poimirlem25  38564  iuneq2f  39089  mpobi123f  39095  mptbi12f  39099  dvdsrabdioph  43817  fphpd  43823  mnringmulrcld  45226  fvelrnbf  46035  refsum2cnlem1  46054  elrnmpt1sf  46204  choicefi  46214  axccdom  46235  uzublem  46440  fsumf1of  46586  fmuldfeq  46595  mccl  46610  climmulf  46616  climexp  46617  climsuse  46620  climrecf  46621  climaddf  46627  mullimc  46628  neglimc  46657  addlimc  46658  0ellimcdiv  46659  climeldmeqmpt  46678  climfveqmpt  46681  climfveqf  46690  climfveqmpt3  46692  climeldmeqf  46693  climeqf  46698  climeldmeqmpt3  46699  limsupubuzlem  46722  limsupequz  46733  dvnmptdivc  46948  dvmptfprod  46955  stoweidlem18  47028  stoweidlem31  47041  stoweidlem55  47065  stoweidlem59  47069  sge0iunmpt  47428  sge0reuz  47457  iundjiun  47470  hoicvrrex  47566  ovnhoilem1  47611  ovnlecvr2  47620  opnvonmbllem1  47642  vonioo  47692  vonicc  47695  smflim  47787  smfpimcclem  47817  smfpimcc  47818  cfsetsnfsetf  48128  ovmpordxf  49451