MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfeq Structured version   Visualization version   GIF version

Theorem nfeq 2920
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
StepHypRef Expression
1 nfnfc.1 . . . 4 𝑥𝐴
21a1i 11 . . 3 (⊤ → 𝑥𝐴)
3 nfeq.2 . . . 4 𝑥𝐵
43a1i 11 . . 3 (⊤ → 𝑥𝐵)
52, 4nfeqd 2917 . 2 (⊤ → Ⅎ𝑥 𝐴 = 𝐵)
65mptru 1548 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  wtru 1542  wnf 1785  wnfc 2887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-cleq 2728  df-nfc 2889
This theorem is referenced by:  nfeq1  2922  nfeq2  2924  nfne  3045  raleqf  3328  rexeqf  3329  rmoeq1f  3395  reueq1f  3396  rabeqf  3438  csbhypf  3884  sbceqg  4369  nffn  6601  nffo  6755  fvmptd3f  6963  mpteqb  6967  fvmptf  6969  eqfnfv2f  6986  dff13f  7202  ovmpos  7502  ov2gf  7503  ovmpodxf  7504  ovmpodf  7510  eqerlem  8681  seqof2  13965  sumeq2ii  15577  sumss  15608  fsumadd  15624  fsummulc2  15668  fsumrelem  15691  prodeq1f  15790  prodeq2ii  15795  fprodmul  15842  fproddiv  15843  txcnp  22969  ptcnplem  22970  cnmpt11  23012  cnmpt21  23020  cnmptcom  23027  mbfeqalem1  25003  mbflim  25030  itgeq1f  25134  itgeqa  25176  dvmptfsum  25337  ulmss  25754  leibpi  26290  o1cxp  26322  lgseisenlem2  26722  nosupbnd1  27060  2ndresdju  31512  aciunf1lem  31525  sigapildsys  32701  bnj1316  33372  bnj1446  33597  bnj1447  33598  bnj1448  33599  bnj1519  33617  bnj1520  33618  bnj1529  33622  subtr  34776  subtr2  34777  bj-sbeqALT  35357  poimirlem25  36093  iuneq2f  36605  mpobi123f  36611  mptbi12f  36615  dvdsrabdioph  41110  fphpd  41116  mnringmulrcld  42489  fvelrnbf  43204  refsum2cnlem1  43223  elrnmpt1sf  43383  choicefi  43396  axccdom  43418  uzublem  43640  fsumf1of  43786  fmuldfeq  43795  mccl  43810  climmulf  43816  climexp  43817  climsuse  43820  climrecf  43821  climaddf  43827  mullimc  43828  neglimc  43859  addlimc  43860  0ellimcdiv  43861  climeldmeqmpt  43880  climfveqmpt  43883  climfveqf  43892  climfveqmpt3  43894  climeldmeqf  43895  climeqf  43900  climeldmeqmpt3  43901  limsupubuzlem  43924  limsupequz  43935  dvnmptdivc  44150  dvmptfprod  44157  dvnprodlem1  44158  stoweidlem18  44230  stoweidlem31  44243  stoweidlem55  44267  stoweidlem59  44271  sge0f1o  44594  sge0iunmpt  44630  sge0reuz  44659  iundjiun  44672  hoicvrrex  44768  ovnhoilem1  44813  ovnlecvr2  44822  opnvonmbllem1  44844  vonioo  44894  vonicc  44897  sssmf  44950  smflim  44989  smfpimcclem  45019  smfpimcc  45020  cfsetsnfsetf  45263  ovmpordxf  46385
  Copyright terms: Public domain W3C validator