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

Step	Hyp	Ref	Expression
1		sseli.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		ssel 3562	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)

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  4938  copsex2ga  5154  issref  5428  2elresin  5916  nfvres  6134  fvco4i  6186  mptrcl  6198  fvmptss  6201  fvmptex  6203  fvmptnf  6210  elfvmptrab1  6213  fvopab4ndm  6215  fvimacnvi  6239  elpreima  6245  iinpreima  6253  ofrfval  6803  ofval  6804  off  6810  nnon  6963  finds  6984  finds2  6986  offres  7054  eqopi  7093  op1steq  7101  dfoprab4  7116  bropopvvv  7142  bropfvvvv  7144  curry1val  7157  curry2val  7161  reldmtpos  7247  wfrlem4  7305  wfrlem10  7311  smores3  7337  smores2  7338  frsuc  7419  nnfi  8038  unifpw  8152  f1opwfi  8153  fival  8201  fi0  8209  dffi2  8212  elfiun  8219  cantnfp1lem1  8458  cantnfp1lem3  8460  epfrs  8490  r1fin  8519  r1tr  8522  r1ordg  8524  r1ord3g  8525  r1val1  8532  tz9.12lem3  8535  tcrank  8630  cplem1  8635  hta  8643  tskwe  8659  cardprclem  8688  r0weon  8718  fodomfi2  8766  alephfplem3  8812  dfac12r  8851  ackbij1lem6  8930  ackbij1lem9  8933  ackbij1lem10  8934  ackbij1lem11  8935  ackbij1lem16  8940  ackbij1lem18  8942  ackbij2  8948  fin23lem24  9027  fin23lem26  9030  fin23lem28  9045  fin23lem30  9047  fin23lem31  9048  isfin1-3  9091  fin1a2lem6  9110  hsmexlem4  9134  hsmexlem5  9135  hsmexlem6  9136  axdc2lem  9153  axdc3lem2  9156  axcclem  9162  ac6num  9184  brdom5  9232  brdom4  9233  canthp1lem2  9354  r1tskina  9483  gruina  9519  grur1a  9520  pinn  9579  0nnq  9625  elpqn  9626  recn  9905  rexr  9964  dedekindle  10080  ltord1  10433  leord1  10434  eqord1  10435  nnre  10904  nncn  10905  nnind  10915  nnnn0  11176  nn0re  11178  nn0cn  11179  nn0xnn0  11244  nnz  11276  nn0z  11277  nnq  11677  qcn  11678  rpre  11715  xrge0nre  12148  difreicc  12175  iccshftri  12178  iccshftli  12180  iccdili  12182  icccntri  12184  fzval2  12200  fzelp1  12263  4fvwrd4  12328  elfzo1  12385  ico01fl0  12482  expcllem  12733  expcl2lem  12734  m1expcl2  12744  bcm1k  12964  bcpasc  12970  hashbclem  13093  swrd0fv0  13292  swrd0fvlsw  13295  cshimadifsn  13426  sqrlem5  13835  cau3lem  13942  caubnd  13946  climconst2  14127  rlimres  14137  lo1res  14138  lo1resb  14143  rlimresb  14144  o1resb  14145  o1of2  14191  o1rlimmul  14197  caurcvg  14255  caucvg  14257  ackbijnn  14399  binomlem  14400  incexclem  14407  divcnvshft  14426  zprod  14506  fprodge1  14565  risefaccllem  14583  fallfaccllem  14584  bpolydiflem  14624  bpoly4  14629  dvdsflip  14877  divalglem8  14961  sadadd  15027  smueqlem  15050  smumul  15053  isprm3  15234  phimullem  15322  prmdiveq  15329  unbenlem  15450  prmrec  15464  vdwnnlem1  15537  vdwnnlem3  15539  ramtcl2  15553  prmgaplem4  15596  cshwshashlem1  15640  isstruct2  15704  structcnvcnv  15706  fvsetsid  15722  strlemor1  15796  imasdsval2  15999  xpsfrnel2  16048  mreunirn  16084  mrcfval  16091  mrisval  16113  isacs2  16137  acsfn  16143  arwval  16516  coafval  16537  coapm  16544  isdrs2  16762  isacs3lem  16989  psssdm2  17038  tsrss  17046  submnd0  17143  nmzsubg  17458  nmznsg  17461  resscntz  17587  cntzmhm  17594  symgtrinv  17715  pmtrdifellem4  17722  psgnpmtr  17753  efginvrel2  17963  efginvrel1  17964  efgsp1  17973  efgsres  17974  efgsfo  17975  frgpinv  18000  frgpupf  18009  frgpup1  18011  subcmn  18065  torsubg  18080  dprd2dlem1  18263  dpjidcl  18280  ablfaclem3  18309  subrgpropd  18637  lssacs  18788  sralmod  19008  psrbaglefi  19193  mplsubglem  19255  ressmpladd  19278  ressmplmul  19279  ressmplvsca  19280  mplmonmul  19285  mplind  19323  ply1bascl  19394  cnsubdrglem  19616  rege0subm  19621  rge0srg  19636  zringunit  19655  znrrg  19733  psgnghm  19745  zrhpsgnevpm  19756  evpmodpmf1o  19761  pmtrodpm  19762  frlmsslsp  19954  islinds4  19993  lmimlbs  19994  lbslcic  19999  mdetralt  20233  mdetunilem7  20243  chfacfpmmulgsum2  20489  basdif0  20568  tgval2  20571  mreclatdemoBAD  20710  ordtbas  20806  ordtrest  20816  ordtrestixx  20836  fincmp  21006  cmpfi  21021  bwth  21023  iuncon  21041  1stcrest  21066  hauslly  21105  kgentop  21155  ptbasin  21190  ptcnplem  21234  infil  21477  filunirn  21496  uzrest  21511  elflim  21585  hauspwpwf1  21601  flffval  21603  fclsval  21622  isfcls  21623  fcfval  21647  alexsubALTlem3  21663  alexsubALTlem4  21664  ustn0  21834  fmucndlem  21905  xmetunirn  21952  blbas  22045  blres  22046  mopnval  22053  setsmstopn  22093  tmsval  22096  tngtopn  22264  qtopbaslem  22372  xrtgioo  22417  reperflem  22429  icccmplem1  22433  reconnlem2  22438  xrge0tsms  22445  icopnfhmeo  22550  icccvx  22557  bndth  22565  reparphti  22605  pcofval  22618  pcoval1  22621  pcoval2  22624  pcoass  22632  pcorevlem  22634  pcorev2  22636  pi1xfrcnv  22665  nmhmcn  22728  csscld  22856  cfilfval  22870  caufval  22881  cfilres  22902  bcthlem1  22929  ivthlem1  23027  ivthlem3  23029  ovolicc2lem3  23094  ovolicc2lem4  23095  ioombl1lem4  23136  vitalilem1  23182  vitalilem1OLD  23183  mbflimsup  23239  i1fima2  23252  i1fd  23254  i1f0  23260  i1f1  23263  itg1addlem4  23272  itg1addlem5  23273  iblmbf  23340  ellimc2  23447  limcres  23456  limcun  23465  dvbsss  23472  perfdvf  23473  dvres2lem  23480  dvaddbr  23507  rolle  23557  cmvth  23558  dvlip  23560  dvlipcn  23561  dvle  23574  lhop1lem  23580  dvfsumle  23588  dvfsumge  23589  dvfsumabs  23590  dvfsumlem2  23594  ftc2  23611  itgparts  23614  itgsubstlem  23615  itgsubst  23616  deg1mul3  23679  coeval  23783  coeeu  23785  dgrval  23788  coef3  23792  coemulc  23815  dgrsub  23832  coecj  23838  dvply2  23845  dvnply  23847  quotval  23851  fta1  23867  plyexmo  23872  aacjcl  23886  taylfval  23917  dvtaylp  23928  abelth  23999  pilem2  24010  pilem3  24011  sinord  24084  recosf1o  24085  resinf1o  24086  tanord1  24087  eff1olem  24098  dvloglem  24194  dvlog  24197  dvlog2lem  24198  advlogexp  24201  logtayl  24206  logtayl2  24208  dvcncxp1  24284  dvcnsqrt  24285  cxpcn3lem  24288  cxpcn3  24289  sqrtcn  24291  loglesqrt  24299  1cubr  24369  acosrecl  24430  rlimcnp2  24493  xrlimcnp  24495  efrlim  24496  jensen  24515  lgamgulmlem2  24556  lgamucov2  24565  basellem4  24610  ppiprm  24677  chtprm  24679  prmorcht  24704  musum  24717  chpchtsum  24744  dchrinvcl  24778  dchrghm  24781  dchrinv  24786  dchrsum2  24793  dchrsum  24794  rplogsumlem2  24974  rpvmasumlem  24976  dchrisum0lem2a  25006  dirith2  25017  pnt  25103  tglng  25241  axlowdimlem6  25627  axlowdimlem16  25637  axlowdimlem17  25638  axlowdim  25641  axeuclidlem  25642  axcontlem2  25645  axcontlem7  25650  axcontlem8  25651  clwwlknprop  26300  clwwisshclww  26335  2wlkonot3v  26402  2spthonot3v  26403  nvvcop  26833  nvex  26850  phnv  27053  sheli  27455  cheli  27473  hhssabloilem  27502  choc1  27570  shintcli  27572  chintcli  27574  shsleji  27613  pjini  27942  mayete3i  27971  dmadjop  28131  nlelshi  28303  cnlnadjeui  28320  cnlnssadj  28323  bdopadj  28325  pjimai  28419  stcl  28459  atelch  28587  disjin  28781  disjin2  28782  fcnvgreu  28855  partfun  28858  f1od2  28887  fcobijfs  28889  xrge0infss  28915  iundisj2fi  28943  nnindf  28952  eliccioo  28970  xrge0mulgnn0  29020  xrge0omnd  29042  gsummptres  29115  prsdm  29288  prsrn  29289  ordtrestNEW  29295  xrge0iifcnv  29307  xrge0iifcv  29308  xrge0iifiso  29309  xrge0iifhom  29311  qqhcn  29363  esumval  29435  gsumesum  29448  esumlub  29449  esumcst  29452  esumfsup  29459  esumcvgre  29480  issgon  29513  elrnsiga  29516  imambfm  29651  br2base  29658  sxbrsigalem0  29660  dya2iocucvr  29673  sxbrsigalem2  29675  sxbrsigalem5  29677  sxbrsiga  29679  omssubadd  29689  sitmcl  29740  oddpwdc  29743  eulerpartlemelr  29746  eulerpartlemgvv  29765  eulerpartlemgh  29767  eulerpartlemgs2  29769  eulerpartlemn  29770  sseqf  29781  ballotlem2  29877  ballotlemfp1  29880  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemfmpn  29883  ballotlemsup  29893  ballotlemfrceq  29917  signswch  29964  bnj1533  30176  bnj1137  30317  bnj1286  30341  bnj1408  30358  bnj1417  30363  subfacp1lem5  30420  cvmsi  30501  mpst123  30691  mpstrcl  30692  msrrcl  30694  elmsta  30699  msubvrs  30711  elmpps  30724  elmthm  30727  bcprod  30877  dfon2lem4  30935  frrlem4  31027  pprodss4v  31161  ivthALT  31500  neibastop2lem  31525  nnssi2  31624  nnssi3  31625  bj-sngltagi  32163  bj-elid  32262  bj-elid2  32263  bj-cmnssmndel  32314  bj-ablssgrpel  32316  bj-ablsscmnel  32318  bj-vecssmodel  32321  bj-rrvecssvecel  32328  bj-rrvecsscmnel  32330  taupilemrplb  32343  icorempt2  32375  elxp8  32395  sin2h  32569  cos2h  32570  tan2h  32571  poimirlem14  32593  poimirlem26  32605  poimirlem27  32606  poimirlem31  32610  poimirlem32  32611  mblfinlem1  32616  cnambfre  32628  dvtan  32630  itg2addnc  32634  itg2gt0cn  32635  ftc1cnnc  32654  ftc2nc  32664  dvasin  32666  dvacos  32667  cover2  32678  sstotbnd2  32743  heibor1lem  32778  heiborlem10  32789  opidonOLD  32821  exidcl  32845  rngosn3  32893  flddivrng  32968  toycom  33278  osumcllem7N  34266  pexmidlem4N  34277  diaintclN  35365  dibintclN  35474  mapd1o  35955  hdmapevec  36145  elrfi  36275  elrfirn  36276  elrfirn2  36277  mrefg3  36289  diophin  36354  diophun  36355  eq0rabdioph  36358  eqrabdioph  36359  pellex  36417  rmxycomplete  36500  jm2.23  36581  aomclem2  36643  fglmod  36661  lsmfgcl  36662  lmhmfgima  36672  lmhmfgsplit  36674  isnumbasabl  36695  dgrsub2  36724  itgocn  36753  acsfn1p  36788  areaquad  36821  elmapintrab  36901  corcltrcl  37050  k0004val0  37472  radcnvrat  37535  uzmptshftfval  37567  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  onfrALTlem2  37782  onfrALTlem2VD  38147  uzwo4  38246  disjinfi  38375  eliccxr  38584  eliccelioc  38594  elicores  38607  sqrlearg  38627  fsumiunss  38642  limcdm0  38685  sumnnodd  38697  fnlimfvre  38741  cncfshift  38759  cncfperiod  38764  icccncfext  38773  dvnprodlem1  38836  dvnprodlem2  38837  itgsin0pilem1  38841  itgsinexplem1  38845  itgsinexp  38846  ditgeqiooicc  38852  itgsubsticclem  38867  itgioocnicc  38869  itgsbtaddcnst  38874  stoweidlem34  38927  stoweidlem41  38934  stoweidlem51  38944  wallispilem2  38959  stirlinglem11  38977  dirkercncflem2  38997  fourierdlem5  39005  fourierdlem9  39009  fourierdlem17  39017  fourierdlem18  39018  fourierdlem20  39020  fourierdlem39  39039  fourierdlem48  39047  fourierdlem49  39048  fourierdlem62  39061  fourierdlem66  39065  fourierdlem68  39067  fourierdlem72  39071  fourierdlem73  39072  fourierdlem81  39080  fourierdlem83  39082  fourierdlem85  39084  fourierdlem87  39086  fourierdlem88  39087  fourierdlem92  39091  fourierdlem95  39094  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  etransclem24  39151  etransclem35  39162  etransclem37  39164  salexct  39228  salgencntex  39237  gsumge0cl  39264  sge0tsms  39273  sge0resplit  39299  sge0split  39302  meaiuninclem  39373  caratheodorylem1  39416  volicorescl  39443  hoidmv1lelem3  39483  opnvonmbllem2  39523  ovolval2  39534  ovolval3  39537  ovolval4lem1  39539  ovolval4lem2  39540  pimiooltgt  39598  sssmf  39625  smfaddlem1  39649  smflimlem2  39658  smfrec  39674  smfdiv  39682  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbnd  40225  pfxfv0  40263  pfxfvlsw  40266  1wlk1walk  40843  pthdivtx  40935  pthdadjvtx  40936  crctcsh1wlkn0lem2  41014  crctcsh1wlkn0lem4  41016  clwwisshclwws  41235  fldhmsubc  41876  fldhmsubcALTV  41895  setrec2lem1  42239