Theorem sseli 3599

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 3597	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 1990   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  sselii  3600  sseldi  3601  elun1  3780  elun2  3781  elopabran  5014  copsex2ga  5231  issref  5509  2elresin  6002  nfvres  6224  fvco4i  6276  mptrcl  6289  fvmptss  6292  fvmptex  6294  fvmptnf  6302  elfvmptrab1  6305  fvopab4ndm  6307  fvimacnvi  6331  elpreima  6337  iinpreima  6345  ofrfval  6905  ofval  6906  off  6912  nnon  7071  finds  7092  finds2  7094  offres  7163  eqopi  7202  op1steq  7210  dfoprab4  7225  bropopvvv  7255  bropfvvvv  7257  curry1val  7270  curry2val  7274  reldmtpos  7360  wfrlem4  7418  wfrlem10  7424  smores3  7450  smores2  7451  frsuc  7532  nnfi  8153  unifpw  8269  f1opwfi  8270  fival  8318  fi0  8326  dffi2  8329  elfiun  8336  cantnfp1lem1  8575  cantnfp1lem3  8577  epfrs  8607  r1fin  8636  r1tr  8639  r1ordg  8641  r1ord3g  8642  r1val1  8649  tz9.12lem3  8652  tcrank  8747  cplem1  8752  hta  8760  tskwe  8776  cardprclem  8805  r0weon  8835  fodomfi2  8883  alephfplem3  8929  dfac12r  8968  ackbij1lem6  9047  ackbij1lem9  9050  ackbij1lem10  9051  ackbij1lem11  9052  ackbij1lem16  9057  ackbij1lem18  9059  ackbij2  9065  fin23lem24  9144  fin23lem26  9147  fin23lem28  9162  fin23lem30  9164  fin23lem31  9165  isfin1-3  9208  fin1a2lem6  9227  hsmexlem4  9251  hsmexlem5  9252  hsmexlem6  9253  axdc2lem  9270  axdc3lem2  9273  axcclem  9279  ac6num  9301  brdom5  9351  brdom4  9352  canthp1lem2  9475  r1tskina  9604  gruina  9640  grur1a  9641  pinn  9700  0nnq  9746  elpqn  9747  recn  10026  rexr  10085  dedekindle  10201  ltord1  10554  leord1  10555  eqord1  10556  nnre  11027  nncn  11028  nnind  11038  nnnn0  11299  nn0re  11301  nn0cn  11302  nn0xnn0  11367  nnz  11399  nn0z  11400  nnq  11801  qcn  11802  rpre  11839  xrge0nre  12277  difreicc  12304  iccshftri  12307  iccshftli  12309  iccdili  12311  icccntri  12313  fzval2  12329  fzelp1  12393  4fvwrd4  12459  elfzo1  12517  ico01fl0  12620  expcllem  12871  expcl2lem  12872  m1expcl2  12882  bcm1k  13102  bcpasc  13108  hashbclem  13236  swrd0fv0  13440  swrd0fvlsw  13443  cshimadifsn  13575  sqrlem5  13987  cau3lem  14094  caubnd  14098  climconst2  14279  rlimres  14289  lo1res  14290  lo1resb  14295  rlimresb  14296  o1resb  14297  o1of2  14343  o1rlimmul  14349  caurcvg  14407  caucvg  14409  ackbijnn  14560  binomlem  14561  incexclem  14568  divcnvshft  14587  zprod  14667  fprodge1  14726  risefaccllem  14744  fallfaccllem  14745  bpolydiflem  14785  bpoly4  14790  dvdsflip  15039  divalglem8  15123  sadadd  15189  smueqlem  15212  smumul  15215  isprm3  15396  phimullem  15484  prmdiveq  15491  unbenlem  15612  prmrec  15626  vdwnnlem1  15699  vdwnnlem3  15701  ramtcl2  15715  prmgaplem4  15758  cshwshashlem1  15802  isstruct2  15867  structcnvcnv  15871  fvsetsid  15890  strlemor1OLD  15969  imasdsval2  16176  xpsfrnel2  16225  mreunirn  16261  mrcfval  16268  mrisval  16290  isacs2  16314  acsfn  16320  arwval  16693  coafval  16714  coapm  16721  isdrs2  16939  isacs3lem  17166  psssdm2  17215  tsrss  17223  submnd0  17320  nmzsubg  17635  nmznsg  17638  resscntz  17764  cntzmhm  17771  symgtrinv  17892  pmtrdifellem4  17899  psgnpmtr  17930  efginvrel2  18140  efginvrel1  18141  efgsp1  18150  efgsres  18151  efgsfo  18152  frgpinv  18177  frgpupf  18186  frgpup1  18188  subcmn  18242  torsubg  18257  dprd2dlem1  18440  dpjidcl  18457  ablfaclem3  18486  subrgpropd  18814  lssacs  18967  sralmod  19187  psrbaglefi  19372  mplsubglem  19434  ressmpladd  19457  ressmplmul  19458  ressmplvsca  19459  mplmonmul  19464  mplind  19502  ply1bascl  19573  cnsubdrglem  19797  rege0subm  19802  rge0srg  19817  zringunit  19836  znrrg  19914  psgnghm  19926  zrhpsgnevpm  19937  evpmodpmf1o  19942  pmtrodpm  19943  frlmsslsp  20135  islinds4  20174  lmimlbs  20175  lbslcic  20180  mdetralt  20414  mdetunilem7  20424  chfacfpmmulgsum2  20670  basdif0  20757  tgval2  20760  mreclatdemoBAD  20900  ordtbas  20996  ordtrest  21006  ordtrestixx  21026  fincmp  21196  cmpfi  21211  bwth  21213  iunconn  21231  1stcrest  21256  hauslly  21295  kgentop  21345  ptbasin  21380  ptcnplem  21424  infil  21667  filunirn  21686  uzrest  21701  elflim  21775  hauspwpwf1  21791  flffval  21793  fclsval  21812  isfcls  21813  fcfval  21837  alexsubALTlem3  21853  alexsubALTlem4  21854  ustn0  22024  fmucndlem  22095  xmetunirn  22142  blbas  22235  blres  22236  mopnval  22243  setsmstopn  22283  tmsval  22286  tngtopn  22454  qtopbaslem  22562  xrtgioo  22609  reperflem  22621  icccmplem1  22625  reconnlem2  22630  xrge0tsms  22637  icopnfhmeo  22742  icccvx  22749  bndth  22757  reparphti  22797  pcofval  22810  pcoval1  22813  pcoval2  22816  pcoass  22824  pcorevlem  22826  pcorev2  22828  pi1xfrcnv  22857  nmhmcn  22920  csscld  23048  cfilfval  23062  caufval  23073  cfilres  23094  bcthlem1  23121  ivthlem1  23220  ivthlem3  23222  ovolicc2lem3  23287  ovolicc2lem4  23288  ioombl1lem4  23329  vitalilem1  23376  vitalilem1OLD  23377  mbflimsup  23433  i1fima2  23446  i1fd  23448  i1f0  23454  i1f1  23457  itg1addlem4  23466  itg1addlem5  23467  iblmbf  23534  ellimc2  23641  limcres  23650  limcun  23659  dvbsss  23666  perfdvf  23667  dvres2lem  23674  dvaddbr  23701  rolle  23753  cmvth  23754  dvlip  23756  dvlipcn  23757  dvle  23770  lhop1lem  23776  dvfsumle  23784  dvfsumge  23785  dvfsumabs  23786  dvfsumlem2  23790  ftc2  23807  itgparts  23810  itgsubstlem  23811  itgsubst  23812  deg1mul3  23875  coeval  23979  coeeu  23981  dgrval  23984  coef3  23988  coemulc  24011  dgrsub  24028  coecj  24034  dvply2  24041  dvnply  24043  quotval  24047  fta1  24063  plyexmo  24068  aacjcl  24082  taylfval  24113  dvtaylp  24124  abelth  24195  pilem2  24206  pilem3  24207  sinord  24280  recosf1o  24281  resinf1o  24282  tanord1  24283  eff1olem  24294  dvloglem  24394  dvlog  24397  dvlog2lem  24398  advlogexp  24401  logtayl  24406  logtayl2  24408  dvcncxp1  24484  dvcnsqrt  24485  cxpcn3lem  24488  cxpcn3  24489  sqrtcn  24491  loglesqrt  24499  1cubr  24569  acosrecl  24630  rlimcnp2  24693  xrlimcnp  24695  efrlim  24696  jensen  24715  lgamgulmlem2  24756  lgamucov2  24765  basellem4  24810  ppiprm  24877  chtprm  24879  prmorcht  24904  musum  24917  chpchtsum  24944  dchrinvcl  24978  dchrghm  24981  dchrinv  24986  dchrsum2  24993  dchrsum  24994  rplogsumlem2  25174  rpvmasumlem  25176  dchrisum0lem2a  25206  dirith2  25217  pnt  25303  tglng  25441  axlowdimlem6  25827  axlowdimlem16  25837  axlowdimlem17  25838  axlowdim  25841  axeuclidlem  25842  axcontlem2  25845  axcontlem7  25850  axcontlem8  25851  wlk1walk  26535  pthdivtx  26625  pthdadjvtx  26626  crctcshwlkn0lem2  26703  crctcshwlkn0lem4  26705  clwwisshclwws  26928  fusgreg2wsp  27200  nvvcop  27449  nvex  27466  phnv  27669  sheli  28071  cheli  28089  hhssabloilem  28118  choc1  28186  shintcli  28188  chintcli  28190  shsleji  28229  pjini  28558  mayete3i  28587  dmadjop  28747  nlelshi  28919  cnlnadjeui  28936  cnlnssadj  28939  bdopadj  28941  pjimai  29035  stcl  29075  atelch  29203  fcnvgreu  29472  f1od2  29499  fcobijfs  29501  xrge0infss  29525  uzssico  29546  iundisj2fi  29556  nnindf  29565  eliccioo  29639  xrge0mulgnn0  29689  xrge0omnd  29711  gsummptres  29784  prsdm  29960  prsrn  29961  ordtrestNEW  29967  xrge0iifcnv  29979  xrge0iifcv  29980  xrge0iifiso  29981  xrge0iifhom  29983  qqhcn  30035  esumval  30108  gsumesum  30121  esumlub  30122  esumcst  30125  esumfsup  30132  esumcvgre  30153  issgon  30186  elrnsiga  30189  imambfm  30324  br2base  30331  sxbrsigalem0  30333  dya2iocucvr  30346  sxbrsigalem2  30348  sxbrsigalem5  30350  sxbrsiga  30352  omssubadd  30362  sitmcl  30413  oddpwdc  30416  eulerpartlemelr  30419  eulerpartlemgvv  30438  eulerpartlemgh  30440  eulerpartlemgs2  30442  eulerpartlemn  30443  sseqf  30454  ballotlem2  30550  ballotlemfp1  30553  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemfmpn  30556  ballotlemsup  30566  ballotlemfrceq  30590  signswch  30638  rpsqrtcn  30671  prodfzo03  30681  itgexpif  30684  bnj1533  30922  bnj1137  31063  bnj1286  31087  bnj1408  31104  bnj1417  31109  subfacp1lem5  31166  cvmsi  31247  mpst123  31437  mpstrcl  31438  msrrcl  31440  elmsta  31445  msubvrs  31457  elmpps  31470  elmthm  31473  bcprod  31624  dfon2lem4  31691  frrlem4  31783  pprodss4v  31991  ivthALT  32330  neibastop2lem  32355  nnssi2  32454  nnssi3  32455  bj-sngltagi  32970  bj-elid  33085  bj-elid2  33086  bj-cmnssmndel  33137  bj-ablssgrpel  33139  bj-ablsscmnel  33141  bj-vecssmodel  33144  bj-rrvecssvecel  33151  bj-rrvecsscmnel  33153  taupilemrplb  33166  icorempt2  33199  elxp8  33219  sin2h  33399  cos2h  33400  tan2h  33401  poimirlem14  33423  poimirlem26  33435  poimirlem27  33436  poimirlem31  33440  poimirlem32  33441  mblfinlem1  33446  cnambfre  33458  dvtan  33460  itg2addnc  33464  itg2gt0cn  33465  ftc1cnnc  33484  ftc2nc  33494  dvasin  33496  dvacos  33497  cover2  33508  sstotbnd2  33573  heibor1lem  33608  heiborlem10  33619  opidonOLD  33651  exidcl  33675  rngosn3  33723  flddivrng  33798  toycom  34260  osumcllem7N  35248  pexmidlem4N  35259  diaintclN  36347  dibintclN  36456  mapd1o  36937  hdmapevec  37127  elrfi  37257  elrfirn  37258  elrfirn2  37259  mrefg3  37271  diophin  37336  diophun  37337  eq0rabdioph  37340  eqrabdioph  37341  pellex  37399  rmxycomplete  37482  jm2.23  37563  aomclem2  37625  fglmod  37643  lsmfgcl  37644  lmhmfgima  37654  lmhmfgsplit  37656  isnumbasabl  37676  dgrsub2  37705  itgocn  37734  acsfn1p  37769  areaquad  37802  elmapintrab  37882  corcltrcl  38031  k0004val0  38452  radcnvrat  38513  uzmptshftfval  38545  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  onfrALTlem2  38761  onfrALTlem2VD  39125  uzwo4  39221  disjinfi  39380  uzublem  39657  eliccxr  39737  eliccelioc  39747  elicores  39760  sqrlearg  39780  fsumiunss  39807  limcdm0  39850  sumnnodd  39862  fnlimfvre  39906  limsupubuzlem  39944  limsupmnflem  39952  limsupre3uzlem  39967  climuzlem  39975  cncfshift  40087  cncfperiod  40092  icccncfext  40100  dvnprodlem1  40161  dvnprodlem2  40162  itgsin0pilem1  40165  itgsinexplem1  40169  itgsinexp  40170  ditgeqiooicc  40176  itgsubsticclem  40191  itgioocnicc  40193  itgsbtaddcnst  40198  stoweidlem34  40251  stoweidlem41  40258  stoweidlem51  40268  wallispilem2  40283  stirlinglem11  40301  dirkercncflem2  40321  fourierdlem5  40329  fourierdlem9  40333  fourierdlem17  40341  fourierdlem18  40342  fourierdlem20  40344  fourierdlem39  40363  fourierdlem48  40371  fourierdlem49  40372  fourierdlem62  40385  fourierdlem66  40389  fourierdlem68  40391  fourierdlem72  40395  fourierdlem73  40396  fourierdlem81  40404  fourierdlem83  40406  fourierdlem85  40408  fourierdlem87  40410  fourierdlem88  40411  fourierdlem92  40415  fourierdlem95  40418  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  sqwvfoura  40445  sqwvfourb  40446  fouriersw  40448  etransclem24  40475  etransclem35  40486  etransclem37  40488  salexct  40552  salgencntex  40561  gsumge0cl  40588  sge0tsms  40597  sge0resplit  40623  sge0split  40626  meaiuninclem  40697  caratheodorylem1  40740  volicorescl  40767  hoidmv1lelem3  40807  opnvonmbllem2  40847  ovolval2  40858  ovolval3  40861  ovolval4lem1  40863  ovolval4lem2  40864  pimiooltgt  40921  sssmf  40947  smfaddlem1  40971  smflimlem2  40980  smfrec  40996  smfdiv  41004  smfsuplem1  41017  smfsuplem3  41019  pfxfv0  41400  pfxfvlsw  41403  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbnd  41697  spr0el  41732  fldhmsubc  42084  fldhmsubcALTV  42102  setrec2lem1  42440