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

Theorem sseli 3962
Description: Membership implication 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 3960 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951
This theorem is referenced by:  sselii  3963  sseldi  3964  elun1  4151  elun2  4152  elopabran  5440  copsex2ga  5674  2elresin  6462  nfvres  6700  fvco4i  6756  mptrcl  6770  fvmptss  6773  fvmptex  6775  fvmptnf  6783  elfvmptrab1w  6787  elfvmptrab1  6788  fvopab4ndm  6790  fvimacnvi  6815  elpreima  6821  iinpreima  6830  ofrfval  7406  ofval  7407  off  7413  nnon  7574  finds  7596  finds2  7598  eqopi  7716  op1steq  7724  dfoprab4  7744  bropopvvv  7776  bropfvvvv  7778  reldmtpos  7891  wfrlem10  7955  smores2  7982  frsuc  8063  nnfi  8700  unifpw  8816  cantnfp1lem1  9130  cantnfp1lem3  9132  r1fin  9191  r1tr  9194  r1ordg  9196  r1ord3g  9197  r1val1  9204  tz9.12lem3  9207  tcrank  9302  cplem1  9307  hta  9315  tskwe  9368  cardprclem  9397  alephfplem3  9521  dfac12r  9561  ackbij1lem16  9646  ackbij2  9654  fin23lem28  9751  fin23lem30  9753  fin23lem31  9754  fin1a2lem6  9816  hsmexlem4  9840  hsmexlem5  9841  hsmexlem6  9842  axdc2lem  9859  axdc3lem2  9862  axcclem  9868  ac6num  9890  brdom5  9940  brdom4  9941  r1tskina  10193  gruina  10229  grur1a  10230  pinn  10289  0nnq  10335  elpqn  10336  recn  10616  rexr  10676  ltord1  11155  leord1  11156  eqord1  11157  nnre  11634  nncn  11635  nnind  11645  nnnn0  11893  nn0re  11895  nn0cn  11896  nn0xnn0  11960  nnz  11993  nn0z  11994  nnq  12351  qcn  12352  rpre  12387  eliccxr  12813  difreicc  12860  iccshftri  12863  iccshftli  12865  iccdili  12867  icccntri  12869  fzval2  12885  fzelp1  12949  4fvwrd4  13017  elfzo1  13077  ico01fl0  13179  expcllem  13430  expcl2lem  13431  m1expcl2  13441  bcm1k  13665  bcpasc  13671  hashbclem  13800  wrdv  13867  pfxfv0  14044  pfxfvlsw  14047  cshimadifsn  14181  swrds2m  14293  sqrlem5  14596  cau3lem  14704  caubnd  14708  climconst2  14895  o1of2  14959  o1rlimmul  14965  caurcvg  15023  caucvg  15025  binomlem  15174  incexclem  15181  divcnvshft  15200  zprod  15281  fprodge1  15339  risefaccllem  15357  fallfaccllem  15358  bpolydiflem  15398  bpoly4  15403  dvdsflip  15657  divalglem8  15741  sadadd  15806  smumul  15832  isprm3  16017  phimullem  16106  prmdiveq  16113  unbenlem  16234  vdwnnlem1  16321  vdwnnlem3  16323  ramtcl2  16337  prmgaplem4  16380  cshwshashlem1  16419  structcnvcnv  16487  fvsetsid  16505  imasdsval2  16779  mreunirn  16862  mrcfval  16869  mrisval  16891  coapm  17321  tsrss  17823  submnd0  17930  nmzsubg  18257  nmznsg  18260  cntzmhm  18409  symgtrinv  18531  pmtrdifellem4  18538  psgnpmtr  18569  efginvrel2  18784  efginvrel1  18785  efgsp1  18794  efgsres  18795  efgsfo  18796  frgpinv  18821  frgpupf  18830  frgpup1  18832  subcmn  18888  torsubg  18905  dprd2dlem1  19094  dpjidcl  19111  ablfaclem3  19140  acsfn1p  19509  lssacs  19670  psrbaglefi  20082  mplsubglem  20144  ressmpladd  20168  ressmplmul  20169  ressmplvsca  20170  mplmonmul  20175  ply1bascl  20301  cnsubdrglem  20526  rege0subm  20531  rge0srg  20546  zringunit  20565  znrrg  20642  psgnghm  20654  zrhpsgnevpm  20665  evpmodpmf1o  20670  pmtrodpm  20671  phlssphl  20733  frlmsslsp  20870  islinds4  20909  lmimlbs  20910  lbslcic  20915  mdetralt  21147  mdetunilem7  21157  chfacfpmmulgsum2  21403  tgval2  21494  ordtbas  21730  ordtrestixx  21760  hauslly  22030  kgentop  22080  ptbasin  22115  filunirn  22420  uzrest  22435  elflim  22509  flffval  22527  fclsval  22546  isfcls  22547  fcfval  22571  ustn0  22758  fmucndlem  22829  xmetunirn  22876  mopnval  22977  setsmstopn  23017  tmsval  23020  tngtopn  23188  qtopbaslem  23296  xrtgioo  23343  reperflem  23355  icccmplem1  23359  icopnfhmeo  23476  icccvx  23483  bndth  23491  reparphti  23530  pcoval1  23546  pcoval2  23549  pcoass  23557  pcorevlem  23559  pcorev2  23561  pi1xfrcnv  23590  csscld  23781  cfilfval  23796  caufval  23807  bcthlem1  23856  ivthlem1  23981  ivthlem3  23983  ovolicc2lem3  24049  ovolicc2lem4  24050  vitalilem1  24138  mbflimsup  24196  i1fd  24211  i1f0  24217  i1f1  24220  itg1addlem4  24229  itg1addlem5  24230  iblmbf  24297  ellimc2  24404  limcres  24413  limcun  24422  dvbsss  24429  perfdvf  24430  dvres2lem  24437  dvaddbr  24464  rolle  24516  cmvth  24517  dvlip  24519  dvlipcn  24520  dvle  24533  lhop1lem  24539  dvfsumle  24547  dvfsumge  24548  dvfsumabs  24549  dvfsumlem2  24553  ftc2  24570  itgparts  24573  itgsubstlem  24574  itgsubst  24575  deg1mul3  24638  coeval  24742  coeeu  24744  dgrval  24747  coef3  24751  coemulc  24774  dgrsub  24791  coecj  24797  dvply2  24804  dvnply  24806  quotval  24810  fta1  24826  plyexmo  24831  aacjcl  24845  taylfval  24876  dvtaylp  24887  abelth  24958  pilem3  24970  sinord  25045  recosf1o  25046  resinf1o  25047  tanord1  25048  eff1olem  25059  dvloglem  25158  dvlog  25161  dvlog2lem  25162  advlogexp  25165  logtayl  25170  logtayl2  25172  dvcncxp1  25251  dvcnsqrt  25252  cxpcn3lem  25255  cxpcn3  25256  sqrtcn  25258  loglesqrt  25266  1cubr  25347  acosrecl  25408  efrlim  25475  jensen  25494  lgamgulmlem2  25535  lgamucov2  25544  basellem4  25589  musum  25696  dchrinvcl  25757  dchrghm  25760  dchrinv  25765  dchrsum2  25772  dchrsum  25773  rpvmasumlem  25991  dchrisum0lem2a  26021  pnt  26118  tglng  26260  axlowdimlem6  26661  axlowdimlem16  26671  axlowdimlem17  26672  axlowdim  26675  axeuclidlem  26676  axcontlem2  26679  axcontlem7  26684  axcontlem8  26685  nbusgrvtxm1uvtx  27115  wlk1walk  27348  pthdivtx  27438  pthdadjvtx  27439  crctcshwlkn0lem2  27517  crctcshwlkn0lem4  27519  clwwisshclwws  27721  fusgreg2wsp  28043  nvvcop  28299  nvex  28316  phnv  28519  sheli  28919  cheli  28937  hhssabloilem  28966  choc1  29032  shintcli  29034  chintcli  29036  shsleji  29075  pjini  29404  mayete3i  29433  dmadjop  29593  nlelshi  29765  cnlnadjeui  29782  cnlnssadj  29785  bdopadj  29787  pjimai  29881  stcl  29921  atelch  30049  fcnvgreu  30347  f1od2  30384  fcobijfs  30386  uzssico  30434  iundisj2fi  30447  nnindf  30462  eliccioo  30535  gsummptres  30618  cyc3genpm  30722  ordtrestNEW  31064  xrge0iifcnv  31076  xrge0iifcv  31077  xrge0iifiso  31078  xrge0iifhom  31080  qqhcn  31132  esumval  31205  gsumesum  31218  esumlub  31219  esumcst  31222  esumfsup  31229  issgon  31282  elrnsiga  31285  imambfm  31420  br2base  31427  sxbrsigalem0  31429  dya2iocucvr  31442  sxbrsigalem2  31444  sxbrsigalem5  31446  sxbrsiga  31448  omssubadd  31458  sitmcl  31509  oddpwdc  31512  eulerpartlemelr  31515  eulerpartlemgvv  31534  eulerpartlemgh  31536  eulerpartlemgs2  31538  eulerpartlemn  31539  sseqf  31550  ballotlem2  31646  ballotlemfp1  31649  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemfmpn  31652  ballotlemsup  31662  ballotlemfrceq  31686  signswch  31731  rpsqrtcn  31764  prodfzo03  31774  itgexpif  31777  bnj1533  32024  bnj1137  32165  bnj1286  32189  bnj1408  32206  bnj1417  32211  subfacp1lem5  32329  cvmsi  32410  gonar  32540  goalr  32542  mpst123  32685  mpstrcl  32686  msrrcl  32688  elmsta  32693  msubvrs  32705  elmpps  32718  elmthm  32721  bcprod  32868  dfon2lem4  32929  pprodss4v  33243  ivthALT  33581  neibastop2lem  33606  nnssi2  33701  nnssi3  33702  bj-sngltagi  34192  bj-elid5  34354  bj-fvmptunsn1  34432  bj-cmnssmndel  34444  bj-grpssmndel  34446  bj-ablssgrpel  34448  bj-ablsscmnel  34450  bj-vecssmodel  34453  bj-rveccvec  34475  bj-rvecabl  34477  taupilemrplb  34484  icorempo  34515  elxp8  34535  sin2h  34764  cos2h  34765  tan2h  34766  poimirlem14  34788  poimirlem26  34800  poimirlem27  34801  poimirlem31  34805  poimirlem32  34806  mblfinlem1  34811  cnambfre  34822  dvtan  34824  itg2addnc  34828  itg2gt0cn  34829  ftc1cnnc  34848  ftc2nc  34858  dvasin  34860  dvacos  34861  cover2  34872  sstotbnd2  34935  heibor1lem  34970  heiborlem10  34981  opidonOLD  35013  exidcl  35037  rngosn3  35085  flddivrng  35160  toycom  35991  osumcllem7N  36980  pexmidlem4N  36991  diaintclN  38076  dibintclN  38185  mapd1o  38666  hdmapevec  38853  prjspvs  39140  prjspeclsp  39142  0prjspnrel  39149  elrfi  39171  elrfirn  39172  elrfirn2  39173  mrefg3  39185  diophin  39249  diophun  39250  eq0rabdioph  39253  eqrabdioph  39254  pellex  39312  rmxycomplete  39394  jm2.23  39473  aomclem2  39535  fglmod  39553  lsmfgcl  39554  lmhmfgima  39564  lmhmfgsplit  39566  isnumbasabl  39586  dgrsub2  39615  itgocn  39644  areaquad  39703  elmapintrab  39816  corcltrcl  39964  k0004val0  40384  elscottab  40460  radcnvrat  40526  uzmptshftfval  40558  binomcxplemdvsum  40567  binomcxplemnotnn0  40568  onfrALTlem2  40760  onfrALTlem2VD  41103  uzwo4  41195  disjinfi  41334  mptssid  41391  uzublem  41584  eliccelioc  41677  elicores  41689  sqrlearg  41709  fsumiunss  41736  limcdm0  41779  sumnnodd  41791  fnlimfvre  41835  limsupubuzlem  41873  limsupmnflem  41881  limsupre3uzlem  41896  climuzlem  41904  cncfshift  42037  cncfperiod  42042  icccncfext  42050  dvnprodlem1  42111  dvnprodlem2  42112  itgsin0pilem1  42115  itgsinexplem1  42119  itgsinexp  42120  ditgeqiooicc  42125  itgsubsticclem  42140  itgioocnicc  42142  itgsbtaddcnst  42147  stoweidlem34  42200  stoweidlem41  42207  stoweidlem51  42217  wallispilem2  42232  stirlinglem11  42250  dirkercncflem2  42270  fourierdlem5  42278  fourierdlem9  42282  fourierdlem17  42290  fourierdlem18  42291  fourierdlem20  42293  fourierdlem39  42312  fourierdlem48  42320  fourierdlem49  42321  fourierdlem62  42334  fourierdlem66  42338  fourierdlem68  42340  fourierdlem72  42344  fourierdlem73  42345  fourierdlem81  42353  fourierdlem83  42355  fourierdlem85  42357  fourierdlem87  42359  fourierdlem88  42360  fourierdlem92  42364  fourierdlem95  42367  fourierdlem103  42375  fourierdlem104  42376  fourierdlem112  42384  sqwvfoura  42394  sqwvfourb  42395  fouriersw  42397  etransclem24  42424  etransclem35  42435  etransclem37  42437  salexct  42498  salgencntex  42507  sge0resplit  42569  sge0split  42572  meaiuninclem  42643  caratheodorylem1  42689  volicorescl  42716  hoidmv1lelem3  42756  opnvonmbllem2  42796  ovolval2  42807  ovolval3  42810  ovolval4lem1  42812  ovolval4lem2  42813  pimiooltgt  42870  sssmf  42896  smfaddlem1  42920  smflimlem2  42929  smfrec  42945  smfdiv  42953  smfsuplem1  42966  smfsuplem3  42968  spr0el  43491  bgoldbtbndlem2  43818  bgoldbtbndlem3  43819  bgoldbtbnd  43821  smndex1id  43981  fldhmsubc  44253  fldhmsubcALTV  44271  setrec2lem1  44694
  Copyright terms: Public domain W3C validator