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

Theorem nfeq 2995
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 2992 . 2 (⊤ → Ⅎ𝑥 𝐴 = 𝐵)
65mptru 1545 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wtru 1539  wnf 1785  wnfc 2962
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 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-cleq 2817  df-nfc 2964
This theorem is referenced by:  nfeq1  2997  nfeq2  2999  nfne  3114  raleqf  3388  rexeqf  3389  reueq1f  3390  rmoeq1f  3391  rabeqf  3466  csbhypf  3894  sbceqg  4344  nffn  6440  nffo  6580  fvmptd3f  6774  mpteqb  6778  fvmptf  6780  eqfnfv2f  6797  dff13f  7006  ovmpos  7291  ov2gf  7292  ovmpodxf  7293  ovmpodf  7299  eqerlem  8319  seqof2  13433  sumeq2ii  15050  sumss  15081  fsumadd  15096  fsummulc2  15139  fsumrelem  15162  prodeq1f  15262  prodeq2ii  15267  fprodmul  15314  fproddiv  15315  txcnp  22228  ptcnplem  22229  cnmpt11  22271  cnmpt21  22279  cnmptcom  22286  mbfeqalem1  24248  mbflim  24275  itgeq1f  24378  itgeqa  24420  dvmptfsum  24581  ulmss  24995  leibpi  25531  o1cxp  25563  lgseisenlem2  25963  aciunf1lem  30418  sigapildsys  31478  bnj1316  32149  bnj1446  32374  bnj1447  32375  bnj1448  32376  bnj1519  32394  bnj1520  32395  bnj1529  32399  nosupbnd1  33271  subtr  33719  subtr2  33720  bj-sbeqALT  34285  poimirlem25  35027  iuneq2f  35539  mpobi123f  35545  mptbi12f  35549  dvdsrabdioph  39667  fphpd  39673  mnringmulrcld  40856  fvelrnbf  41567  refsum2cnlem1  41586  elrnmpt1sf  41741  choicefi  41754  axccdom  41778  uzublem  41993  fsumf1of  42142  fmuldfeq  42151  mccl  42166  climmulf  42172  climexp  42173  climsuse  42176  climrecf  42177  climaddf  42183  mullimc  42184  neglimc  42215  addlimc  42216  0ellimcdiv  42217  climeldmeqmpt  42236  climfveqmpt  42239  climfveqf  42248  climfveqmpt3  42250  climeldmeqf  42251  climeqf  42256  climeldmeqmpt3  42257  limsupubuzlem  42280  limsupequz  42291  dvnmptdivc  42506  dvmptfprod  42513  dvnprodlem1  42514  stoweidlem18  42586  stoweidlem31  42599  stoweidlem55  42623  stoweidlem59  42627  sge0f1o  42947  sge0iunmpt  42983  sge0reuz  43012  iundjiun  43025  hoicvrrex  43121  ovnhoilem1  43166  ovnlecvr2  43175  opnvonmbllem1  43197  vonioo  43247  vonicc  43250  sssmf  43298  smflim  43336  smfpimcclem  43364  smfpimcc  43365  ovmpordxf  44666
  Copyright terms: Public domain W3C validator