Theorem nfeq 2937

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

Syntax hints:   = wceq 1560  ⊤wtru 1561  Ⅎwnf 1803  Ⅎwnfc 2909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-nf 1804  df-cleq 2754  df-nfc 2911

This theorem is referenced by:  nfeq1  2939  nfeq2  2941  nfne  3058  raleqf  3343  rmoeq1f  3404  rabeqf  3448  csbhypf  3880  sbceqg  4366  nffn  6620  nffo  6777  fvmptd3f  6991  mpteqb  6995  fvmptf  6997  eqfnfv2f  7015  dff13f  7239  ovmpos  7544  ov2gf  7545  ovmpodxf  7546  ovmpodf  7552  eqerlem  8714  seqof2  14073  sumeq2ii  15720  sumss  15751  fsumadd  15767  fsummulc2  15811  fsumrelem  15835  prodeq1f  15936  prodeq2ii  15941  fprodmul  15990  fproddiv  15991  txcnp  23677  ptcnplem  23678  cnmpt11  23720  cnmpt21  23728  cnmptcom  23735  mbfeqalem1  25700  mbflim  25727  itgeq1f  25830  itgeq1fOLD  25831  itgeqa  25873  dvmptfsum  26034  ulmss  26457  leibpi  27004  o1cxp  27036  lgseisenlem2  27437  nosupbnd1  27775  2ndresdju  32848  aciunf1lem  32861  deg1prod  33776  sigapildsys  34456  bnj1316  35112  bnj1446  35337  bnj1447  35338  bnj1448  35339  bnj1519  35357  bnj1520  35358  bnj1529  35362  subtr  36671  subtr2  36672  bj-sbeqALT  37382  poimirlem25  38141  iuneq2f  38652  mpobi123f  38658  mptbi12f  38662  dvdsrabdioph  43384  fphpd  43390  mnringmulrcld  44801  fvelrnbf  45595  refsum2cnlem1  45614  elrnmpt1sf  45764  choicefi  45774  axccdom  45795  uzublem  46001  fsumf1of  46147  fmuldfeq  46156  mccl  46171  climmulf  46177  climexp  46178  climsuse  46181  climrecf  46182  climaddf  46188  mullimc  46189  neglimc  46218  addlimc  46219  0ellimcdiv  46220  climeldmeqmpt  46239  climfveqmpt  46242  climfveqf  46251  climfveqmpt3  46253  climeldmeqf  46254  climeqf  46259  climeldmeqmpt3  46260  limsupubuzlem  46283  limsupequz  46294  dvnmptdivc  46509  dvmptfprod  46516  stoweidlem18  46589  stoweidlem31  46602  stoweidlem55  46626  stoweidlem59  46630  sge0iunmpt  46989  sge0reuz  47018  iundjiun  47031  hoicvrrex  47127  ovnhoilem1  47172  ovnlecvr2  47181  opnvonmbllem1  47203  vonioo  47253  vonicc  47256  smflim  47348  smfpimcclem  47378  smfpimcc  47379  cfsetsnfsetf  47649  ovmpordxf  48958