MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tsetndx Unicode version

Theorem tsetndx 14168
Description: Index value of the df-tset 14102 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
Assertion
Ref Expression
tsetndx

Proof of Theorem tsetndx
StepHypRef Expression
1 df-tset 14102 . 2
2 9nn 10352 . 2
31, 2ndxarg 14041 1
Colors of variables: wff set class
Syntax hints:  =wceq 1670  `cfv 5438  9c9 10244   cnx 14018   cts 14089
This theorem is referenced by:  topgrpstr  14170  otpsstr  14177  odrngstr  14188  imasvalstr  14229  ipostr  15164  psrvalstr  17055  cnfldstr  17330  indistpsx  18088  tuslem  19312  setsmsbas  19520  setsmsds  19521  tnglem  19696  tngds  19704  zlmtset  25574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554  ax-un 6382  ax-cnex 9217  ax-resscn 9218  ax-1cn 9219  ax-icn 9220  ax-addcl 9221  ax-addrcl 9222  ax-mulcl 9223  ax-mulrcl 9224  ax-i2m1 9229  ax-1ne0 9230  ax-rrecex 9233  ax-cnre 9234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-ral 2764  df-rex 2765  df-reu 2766  df-rab 2768  df-v 3017  df-sbc 3225  df-csb 3326  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-pss 3381  df-nul 3674  df-if 3826  df-pw 3895  df-sn 3915  df-pr 3916  df-tp 3917  df-op 3918  df-uni 4118  df-iun 4199  df-br 4319  df-opab 4377  df-mpt 4378  df-tr 4412  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-res 4874  df-ima 4875  df-iota 5401  df-fun 5440  df-fn 5441  df-f 5442  df-f1 5443  df-fo 5444  df-f1o 5445  df-fv 5446  df-ov 6106  df-om 6487  df-recs 6795  df-rdg 6830  df-nn 10189  df-2 10246  df-3 10247  df-4 10248  df-5 10249  df-6 10250  df-7 10251  df-8 10252  df-9 10253  df-ndx 14024  df-slot 14025  df-tset 14102
  Copyright terms: Public domain W3C validator