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

Theorem sseli 3564
Description: Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
sseli.1 𝐴𝐵
Assertion
Ref Expression
sseli (𝐶𝐴𝐶𝐵)

Proof of Theorem sseli
StepHypRef Expression
1 sseli.1 . 2 𝐴𝐵
2 ssel 3562 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  sselii  3565  sseldi  3566  elun1  3742  elun2  3743  elopabran  4928  copsex2ga  5143  issref  5415  2elresin  5902  nfvres  6119  fvco4i  6171  mptrcl  6183  fvmptss  6186  fvmptex  6188  fvmptnf  6195  elfvmptrab1  6198  fvopab4ndm  6200  fvimacnvi  6224  elpreima  6230  iinpreima  6238  ofrfval  6781  ofval  6782  off  6788  nnon  6941  finds  6962  finds2  6964  offres  7032  eqopi  7071  op1steq  7079  dfoprab4  7094  bropopvvv  7120  bropfvvvv  7122  curry1val  7135  curry2val  7139  reldmtpos  7225  wfrlem4  7283  wfrlem10  7289  smores3  7315  smores2  7316  frsuc  7397  nnfi  8016  unifpw  8130  f1opwfi  8131  fival  8179  fi0  8187  dffi2  8190  elfiun  8197  cantnfp1lem1  8436  cantnfp1lem3  8438  epfrs  8468  r1fin  8497  r1tr  8500  r1ordg  8502  r1ord3g  8503  r1val1  8510  tz9.12lem3  8513  tcrank  8608  cplem1  8613  hta  8621  tskwe  8637  cardprclem  8666  r0weon  8696  fodomfi2  8744  alephfplem3  8790  dfac12r  8829  ackbij1lem6  8908  ackbij1lem9  8911  ackbij1lem10  8912  ackbij1lem11  8913  ackbij1lem16  8918  ackbij1lem18  8920  ackbij2  8926  fin23lem24  9005  fin23lem26  9008  fin23lem28  9023  fin23lem30  9025  fin23lem31  9026  isfin1-3  9069  fin1a2lem6  9088  hsmexlem4  9112  hsmexlem5  9113  hsmexlem6  9114  axdc2lem  9131  axdc3lem2  9134  axcclem  9140  ac6num  9162  brdom5  9210  brdom4  9211  canthp1lem2  9332  r1tskina  9461  gruina  9497  grur1a  9498  pinn  9557  0nnq  9603  elpqn  9604  recn  9883  rexr  9942  dedekindle  10053  ltord1  10406  leord1  10407  eqord1  10408  nnre  10877  nncn  10878  nnind  10888  nnnn0  11149  nn0re  11151  nn0cn  11152  nnz  11235  nn0z  11236  nnq  11636  qcn  11637  rpre  11674  xrge0nre  12107  difreicc  12134  iccshftri  12137  iccshftli  12139  iccdili  12141  icccntri  12143  fzval2  12158  fzelp1  12221  4fvwrd4  12286  elfzo1  12343  ico01fl0  12440  expcllem  12691  expcl2lem  12692  m1expcl2  12702  bcm1k  12922  bcpasc  12928  hashbclem  13048  swrd0fv0  13241  swrd0fvlsw  13244  cshimadifsn  13375  sqrlem5  13784  cau3lem  13891  caubnd  13895  climconst2  14076  rlimres  14086  lo1res  14087  lo1resb  14092  rlimresb  14093  o1resb  14094  o1of2  14140  o1rlimmul  14146  caurcvg  14204  caucvg  14206  ackbijnn  14348  binomlem  14349  incexclem  14356  divcnvshft  14375  zprod  14455  fprodge1  14514  risefaccllem  14532  fallfaccllem  14533  bpolydiflem  14573  bpoly4  14578  dvdsflip  14826  divalglem8  14910  sadadd  14976  smueqlem  14999  smumul  15002  isprm3  15183  phimullem  15271  prmdiveq  15278  unbenlem  15399  prmrec  15413  vdwnnlem1  15486  vdwnnlem3  15488  ramtcl2  15502  prmgaplem4  15545  cshwshashlem1  15589  isstruct2  15653  structcnvcnv  15655  fvsetsid  15671  strlemor1  15745  imasdsval2  15948  xpsfrnel2  15997  mreunirn  16033  mrcfval  16040  mrisval  16062  isacs2  16086  acsfn  16092  arwval  16465  coafval  16486  coapm  16493  isdrs2  16711  isacs3lem  16938  psssdm2  16987  tsrss  16995  submnd0  17092  nmzsubg  17407  nmznsg  17410  resscntz  17536  cntzmhm  17543  symgtrinv  17664  pmtrdifellem4  17671  psgnpmtr  17702  efginvrel2  17912  efginvrel1  17913  efgsp1  17922  efgsres  17923  efgsfo  17924  frgpinv  17949  frgpupf  17958  frgpup1  17960  subcmn  18014  torsubg  18029  dprd2dlem1  18212  dpjidcl  18229  ablfaclem3  18258  subrgpropd  18586  lssacs  18737  sralmod  18957  psrbaglefi  19142  mplsubglem  19204  ressmpladd  19227  ressmplmul  19228  ressmplvsca  19229  mplmonmul  19234  mplind  19272  ply1bascl  19343  cnsubdrglem  19565  rege0subm  19570  rge0srg  19585  zringunit  19606  znrrg  19681  psgnghm  19693  zrhpsgnevpm  19704  evpmodpmf1o  19709  pmtrodpm  19710  frlmsslsp  19902  islinds4  19941  lmimlbs  19942  lbslcic  19947  mdetralt  20181  mdetunilem7  20191  chfacfpmmulgsum2  20437  basdif0  20516  tgval2  20519  mreclatdemoBAD  20658  ordtbas  20754  ordtrest  20764  ordtrestixx  20784  fincmp  20954  cmpfi  20969  bwth  20971  iuncon  20989  1stcrest  21014  hauslly  21053  kgentop  21103  ptbasin  21138  ptcnplem  21182  infil  21425  filunirn  21444  uzrest  21459  elflim  21533  hauspwpwf1  21549  flffval  21551  fclsval  21570  isfcls  21571  fcfval  21595  alexsubALTlem3  21611  alexsubALTlem4  21612  ustn0  21782  fmucndlem  21853  xmetunirn  21900  blbas  21993  blres  21994  mopnval  22001  setsmstopn  22041  tmsval  22044  tngtopn  22212  qtopbaslem  22320  xrtgioo  22365  reperflem  22377  icccmplem1  22381  reconnlem2  22386  xrge0tsms  22393  icopnfhmeo  22498  icccvx  22505  bndth  22513  reparphti  22553  pcofval  22566  pcoval1  22569  pcoval2  22572  pcoass  22580  pcorevlem  22582  pcorev2  22584  pi1xfrcnv  22613  nmhmcn  22676  csscld  22801  cfilfval  22815  caufval  22826  cfilres  22847  bcthlem1  22874  ivthlem1  22972  ivthlem3  22974  ovolicc2lem3  23039  ovolicc2lem4  23040  ioombl1lem4  23081  vitalilem1  23127  vitalilem1OLD  23128  mbflimsup  23184  i1fima2  23197  i1fd  23199  i1f0  23205  i1f1  23208  itg1addlem4  23217  itg1addlem5  23218  iblmbf  23285  ellimc2  23392  limcres  23401  limcun  23410  dvbsss  23417  perfdvf  23418  dvres2lem  23425  dvaddbr  23452  rolle  23502  cmvth  23503  dvlip  23505  dvlipcn  23506  dvle  23519  lhop1lem  23525  dvfsumle  23533  dvfsumge  23534  dvfsumabs  23535  dvfsumlem2  23539  ftc2  23556  itgparts  23559  itgsubstlem  23560  itgsubst  23561  deg1mul3  23624  coeval  23728  coeeu  23730  dgrval  23733  coef3  23737  coemulc  23760  dgrsub  23777  coecj  23783  dvply2  23790  dvnply  23792  quotval  23796  fta1  23812  plyexmo  23817  aacjcl  23831  taylfval  23862  dvtaylp  23873  abelth  23944  pilem2  23955  pilem3  23956  sinord  24029  recosf1o  24030  resinf1o  24031  tanord1  24032  eff1olem  24043  dvloglem  24139  dvlog  24142  dvlog2lem  24143  advlogexp  24146  logtayl  24151  logtayl2  24153  dvcncxp1  24229  dvcnsqrt  24230  cxpcn3lem  24233  cxpcn3  24234  sqrtcn  24236  loglesqrt  24244  1cubr  24314  acosrecl  24375  rlimcnp2  24438  xrlimcnp  24440  efrlim  24441  jensen  24460  lgamgulmlem2  24501  lgamucov2  24510  basellem4  24555  ppiprm  24622  chtprm  24624  prmorcht  24649  musum  24662  chpchtsum  24689  dchrinvcl  24723  dchrghm  24726  dchrinv  24731  dchrsum2  24738  dchrsum  24739  rplogsumlem2  24919  rpvmasumlem  24921  dchrisum0lem2a  24951  dirith2  24962  pnt  25048  tglng  25187  axlowdimlem6  25573  axlowdimlem16  25583  axlowdimlem17  25584  axlowdim  25587  axeuclidlem  25588  axcontlem2  25591  axcontlem7  25596  axcontlem8  25597  clwwlknprop  26094  clwwisshclww  26129  2wlkonot3v  26196  2spthonot3v  26197  nvvcop  26627  nvex  26644  phnv  26847  sheli  27249  cheli  27267  hhssabloilem  27296  choc1  27364  shintcli  27366  chintcli  27368  shsleji  27407  pjini  27736  mayete3i  27765  dmadjop  27925  nlelshi  28097  cnlnadjeui  28114  cnlnssadj  28117  bdopadj  28119  pjimai  28213  stcl  28253  atelch  28381  disjin  28575  disjin2  28576  fcnvgreu  28649  partfun  28652  f1od2  28681  fcobijfs  28683  xrge0infss  28709  iundisj2fi  28737  nnindf  28746  eliccioo  28764  xrge0mulgnn0  28814  xrge0omnd  28836  gsummptres  28909  prsdm  29082  prsrn  29083  ordtrestNEW  29089  xrge0iifcnv  29101  xrge0iifcv  29102  xrge0iifiso  29103  xrge0iifhom  29105  qqhcn  29157  esumval  29229  gsumesum  29242  esumlub  29243  esumcst  29246  esumfsup  29253  esumcvgre  29274  issgon  29307  elrnsiga  29310  imambfm  29445  br2base  29452  sxbrsigalem0  29454  dya2iocucvr  29467  sxbrsigalem2  29469  sxbrsigalem5  29471  sxbrsiga  29473  omssubadd  29483  sitmcl  29534  oddpwdc  29537  eulerpartlemelr  29540  eulerpartlemgvv  29559  eulerpartlemgh  29561  eulerpartlemgs2  29563  eulerpartlemn  29564  sseqf  29575  ballotlem2  29671  ballotlemfp1  29674  ballotlemfc0  29675  ballotlemfcc  29676  ballotlemfmpn  29677  ballotlemsup  29687  ballotlemfrceq  29711  signswch  29758  bnj1533  29970  bnj1137  30111  bnj1286  30135  bnj1408  30152  bnj1417  30157  subfacp1lem5  30214  cvmsi  30295  mpst123  30485  mpstrcl  30486  msrrcl  30488  elmsta  30493  msubvrs  30505  elmpps  30518  elmthm  30521  bcprod  30671  dfon2lem4  30729  frrlem4  30821  pprodss4v  30955  ivthALT  31294  neibastop2lem  31319  nnssi2  31418  nnssi3  31419  bj-sngltagi  31957  bj-elid  32056  bj-elid2  32057  bj-cmnssmndel  32108  bj-ablssgrpel  32110  bj-ablsscmnel  32112  bj-vecssmodel  32115  bj-rrvecssvecel  32122  bj-rrvecsscmnel  32124  taupilemrplb  32137  icorempt2  32169  elxp8  32189  sin2h  32363  cos2h  32364  tan2h  32365  poimirlem14  32387  poimirlem26  32399  poimirlem27  32400  poimirlem31  32404  poimirlem32  32405  mblfinlem1  32410  cnambfre  32422  dvtan  32424  itg2addnc  32428  itg2gt0cn  32429  ftc1cnnc  32448  ftc2nc  32458  dvasin  32460  dvacos  32461  cover2  32472  sstotbnd2  32537  heibor1lem  32572  heiborlem10  32583  opidonOLD  32615  exidcl  32639  rngosn3  32687  flddivrng  32762  toycom  33072  osumcllem7N  34060  pexmidlem4N  34071  diaintclN  35159  dibintclN  35268  mapd1o  35749  hdmapevec  35939  elrfi  36069  elrfirn  36070  elrfirn2  36071  mrefg3  36083  diophin  36148  diophun  36149  eq0rabdioph  36152  eqrabdioph  36153  pellex  36211  rmxycomplete  36294  jm2.23  36375  aomclem2  36437  fglmod  36455  lsmfgcl  36456  lmhmfgima  36466  lmhmfgsplit  36468  isnumbasabl  36489  dgrsub2  36518  itgocn  36547  acsfn1p  36582  areaquad  36615  elmapintrab  36695  corcltrcl  36844  k0004val0  37266  radcnvrat  37329  uzmptshftfval  37361  binomcxplemdvsum  37370  binomcxplemnotnn0  37371  onfrALTlem2  37576  onfrALTlem2VD  37941  uzwo4  38040  disjinfi  38169  eliccxr  38378  eliccelioc  38388  elicores  38401  sqrlearg  38421  fsumiunss  38436  limcdm0  38479  sumnnodd  38491  fnlimfvre  38535  cncfshift  38553  cncfperiod  38558  icccncfext  38567  dvnprodlem1  38630  dvnprodlem2  38631  itgsin0pilem1  38635  itgsinexplem1  38639  itgsinexp  38640  ditgeqiooicc  38646  itgsubsticclem  38661  itgioocnicc  38663  itgsbtaddcnst  38668  stoweidlem34  38721  stoweidlem41  38728  stoweidlem51  38738  wallispilem2  38753  stirlinglem11  38771  dirkercncflem2  38791  fourierdlem5  38799  fourierdlem9  38803  fourierdlem17  38811  fourierdlem18  38812  fourierdlem20  38814  fourierdlem39  38833  fourierdlem48  38841  fourierdlem49  38842  fourierdlem62  38855  fourierdlem66  38859  fourierdlem68  38861  fourierdlem72  38865  fourierdlem73  38866  fourierdlem81  38874  fourierdlem83  38876  fourierdlem85  38878  fourierdlem87  38880  fourierdlem88  38881  fourierdlem92  38885  fourierdlem95  38888  fourierdlem103  38896  fourierdlem104  38897  fourierdlem112  38905  sqwvfoura  38915  sqwvfourb  38916  fouriersw  38918  etransclem24  38945  etransclem35  38956  etransclem37  38958  salexct  39022  salgencntex  39031  gsumge0cl  39058  sge0tsms  39067  sge0resplit  39093  sge0split  39096  meaiuninclem  39167  caratheodorylem1  39210  volicorescl  39237  hoidmv1lelem3  39277  opnvonmbllem2  39317  ovolval2  39328  ovolval3  39331  ovolval4lem1  39333  ovolval4lem2  39334  pimiooltgt  39392  sssmf  39419  smfaddlem1  39443  smflimlem2  39452  smfrec  39468  smfdiv  39476  bgoldbtbndlem2  40017  bgoldbtbndlem3  40018  bgoldbtbnd  40020  pfxfv0  40058  pfxfvlsw  40061  nn0xnn0  40193  1wlk1walk  40835  pthdivtx  40927  pthdadjvtx  40928  crctcsh1wlkn0lem2  41006  crctcsh1wlkn0lem4  41008  clwwisshclwws  41227  fldhmsubc  41868  fldhmsubcALTV  41887
  Copyright terms: Public domain W3C validator