Theorem sseli 3794

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

Syntax hints:   → wi 4   ∈ wcel 2156   ⊆ wss 3769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783

This theorem is referenced by:  sselii  3795  sseldi  3796  elun1  3979  elun2  3980  elopabran  5209  copsex2ga  5432  idrefOLD  5720  2elresin  6209  nfvres  6440  fvco4i  6493  mptrcl  6506  fvmptss  6509  fvmptex  6511  fvmptnf  6519  elfvmptrab1  6522  fvopab4ndm  6524  fvimacnvi  6549  elpreima  6555  iinpreima  6563  ofrfval  7131  ofval  7132  off  7138  nnon  7297  finds  7318  finds2  7320  offres  7389  eqopi  7430  op1steq  7438  dfoprab4  7453  bropopvvv  7485  bropfvvvv  7487  curry1val  7500  curry2val  7504  reldmtpos  7591  wfrlem4OLD  7650  wfrlem10  7656  smores3  7682  smores2  7683  frsuc  7764  nnfi  8388  unifpw  8504  f1opwfi  8505  fival  8553  fi0  8561  dffi2  8564  elfiun  8571  cantnfp1lem1  8818  cantnfp1lem3  8820  epfrs  8850  r1fin  8879  r1tr  8882  r1ordg  8884  r1ord3g  8885  r1val1  8892  tz9.12lem3  8895  tcrank  8990  cplem1  8995  hta  9003  tskwe  9055  cardprclem  9084  r0weon  9114  fodomfi2  9162  alephfplem3  9208  dfac12r  9249  ackbij1lem6  9328  ackbij1lem9  9331  ackbij1lem10  9332  ackbij1lem11  9333  ackbij1lem16  9338  ackbij1lem18  9340  ackbij2  9346  fin23lem24  9425  fin23lem26  9428  fin23lem28  9443  fin23lem30  9445  fin23lem31  9446  isfin1-3  9489  fin1a2lem6  9508  hsmexlem4  9532  hsmexlem5  9533  hsmexlem6  9534  axdc2lem  9551  axdc3lem2  9554  axcclem  9560  ac6num  9582  brdom5  9632  brdom4  9633  canthp1lem2  9756  r1tskina  9885  gruina  9921  grur1a  9922  pinn  9981  0nnq  10027  elpqn  10028  recn  10307  rexr  10366  dedekindle  10482  ltord1  10835  leord1  10836  eqord1  10837  nnre  11308  nncn  11309  nnind  11319  nnnn0  11562  nn0re  11564  nn0cn  11565  nn0xnn0  11629  nnz  11661  nn0z  11662  nnq  12016  qcn  12017  rpre  12049  eliccxr  12474  difreicc  12523  iccshftri  12526  iccshftli  12528  iccdili  12530  icccntri  12532  fzval2  12548  fzelp1  12612  4fvwrd4  12679  elfzo1  12738  ico01fl0  12840  expcllem  13090  expcl2lem  13091  m1expcl2  13101  bcm1k  13318  bcpasc  13324  hashbclem  13449  swrd0fv0  13660  swrd0fvlsw  13663  cshimadifsn  13795  swrds2m  13906  sqrlem5  14206  cau3lem  14313  caubnd  14317  climconst2  14498  rlimres  14508  lo1res  14509  lo1resb  14514  rlimresb  14515  o1resb  14516  o1of2  14562  o1rlimmul  14568  caurcvg  14626  caucvg  14628  ackbijnn  14778  binomlem  14779  incexclem  14786  divcnvshft  14805  zprod  14884  fprodge1  14942  risefaccllem  14960  fallfaccllem  14961  bpolydiflem  15001  bpoly4  15006  dvdsflip  15258  divalglem8  15339  sadadd  15404  smueqlem  15427  smumul  15430  isprm3  15610  phimullem  15697  prmdiveq  15704  unbenlem  15825  prmrec  15839  vdwnnlem1  15912  vdwnnlem3  15914  ramtcl2  15928  prmgaplem4  15971  cshwshashlem1  16010  isstruct2  16074  structcnvcnv  16078  fvsetsid  16097  strlemor1OLD  16176  imasdsval2  16377  xpsfrnel2  16426  mreunirn  16462  mrcfval  16469  mrisval  16491  isacs2  16514  acsfn  16520  arwval  16893  coafval  16914  coapm  16921  isdrs2  17140  isacs3lem  17367  tsrss  17424  submnd0  17521  nmzsubg  17833  nmznsg  17836  resscntz  17961  cntzmhm  17968  symgtrinv  18089  pmtrdifellem4  18096  psgnpmtr  18127  efginvrel2  18337  efginvrel1  18338  efgsp1  18347  efgsres  18348  efgsfo  18349  frgpinv  18374  frgpupf  18383  frgpup1  18385  subcmn  18439  torsubg  18454  dprd2dlem1  18638  dpjidcl  18655  ablfaclem3  18684  subrgpropd  19014  lssacs  19170  sralmod  19392  psrbaglefi  19577  mplsubglem  19639  ressmpladd  19662  ressmplmul  19663  ressmplvsca  19664  mplmonmul  19669  mplind  19706  ply1bascl  19777  cnsubdrglem  20001  rege0subm  20006  rge0srg  20021  zringunit  20040  znrrg  20117  psgnghm  20129  zrhpsgnevpm  20140  evpmodpmf1o  20146  pmtrodpm  20147  frlmsslsp  20341  islinds4  20380  lmimlbs  20381  lbslcic  20386  mdetralt  20621  mdetunilem7  20631  chfacfpmmulgsum2  20879  basdif0  20967  tgval2  20970  mreclatdemoBAD  21110  ordtbas  21206  ordtrest  21216  ordtrestixx  21236  fincmp  21406  cmpfi  21421  bwth  21423  iunconn  21441  1stcrest  21466  hauslly  21505  kgentop  21555  ptbasin  21590  ptcnplem  21634  infil  21876  filunirn  21895  uzrest  21910  elflim  21984  hauspwpwf1  22000  flffval  22002  fclsval  22021  isfcls  22022  fcfval  22046  alexsubALTlem3  22062  alexsubALTlem4  22063  ustn0  22233  fmucndlem  22304  xmetunirn  22351  blbas  22444  blres  22445  mopnval  22452  setsmstopn  22492  tmsval  22495  tngtopn  22663  qtopbaslem  22771  xrtgioo  22818  reperflem  22830  icccmplem1  22834  reconnlem2  22839  xrge0tsms  22846  icopnfhmeo  22951  icccvx  22958  bndth  22966  reparphti  23005  pcofval  23018  pcoval1  23021  pcoval2  23024  pcoass  23032  pcorevlem  23034  pcorev2  23036  pi1xfrcnv  23065  nmhmcn  23128  csscld  23256  cfilfval  23270  caufval  23281  cfilres  23302  bcthlem1  23329  ivthlem1  23428  ivthlem3  23430  ovolicc2lem3  23496  ovolicc2lem4  23497  ioombl1lem4  23538  vitalilem1  23585  mbflimsup  23643  i1fima2  23656  i1fd  23658  i1f0  23664  i1f1  23667  itg1addlem4  23676  itg1addlem5  23677  iblmbf  23744  ellimc2  23851  limcres  23860  limcun  23869  dvbsss  23876  perfdvf  23877  dvres2lem  23884  dvaddbr  23911  rolle  23963  cmvth  23964  dvlip  23966  dvlipcn  23967  dvle  23980  lhop1lem  23986  dvfsumle  23994  dvfsumge  23995  dvfsumabs  23996  dvfsumlem2  24000  ftc2  24017  itgparts  24020  itgsubstlem  24021  itgsubst  24022  deg1mul3  24085  coeval  24189  coeeu  24191  dgrval  24194  coef3  24198  coemulc  24221  dgrsub  24238  coecj  24244  dvply2  24251  dvnply  24253  quotval  24257  fta1  24273  plyexmo  24278  aacjcl  24292  taylfval  24323  dvtaylp  24334  abelth  24405  pilem3  24417  pilem3OLD  24418  sinord  24491  recosf1o  24492  resinf1o  24493  tanord1  24494  eff1olem  24505  dvloglem  24604  dvlog  24607  dvlog2lem  24608  advlogexp  24611  logtayl  24616  logtayl2  24618  dvcncxp1  24694  dvcnsqrt  24695  cxpcn3lem  24698  cxpcn3  24699  sqrtcn  24701  loglesqrt  24709  1cubr  24779  acosrecl  24840  rlimcnp2  24903  xrlimcnp  24905  efrlim  24906  jensen  24925  lgamgulmlem2  24966  lgamucov2  24975  basellem4  25020  ppiprm  25087  chtprm  25089  prmorcht  25114  musum  25127  chpchtsum  25154  dchrinvcl  25188  dchrghm  25191  dchrinv  25196  dchrsum2  25203  dchrsum  25204  rplogsumlem2  25384  rpvmasumlem  25386  dchrisum0lem2a  25416  dirith2  25427  pnt  25513  tglng  25651  axlowdimlem6  26037  axlowdimlem16  26047  axlowdimlem17  26048  axlowdim  26051  axeuclidlem  26052  axcontlem2  26055  axcontlem7  26060  axcontlem8  26061  nbusgrvtxm1uvtx  26524  wlk1walk  26759  pthdivtx  26849  pthdadjvtx  26850  crctcshwlkn0lem2  26928  crctcshwlkn0lem4  26930  clwwisshclwws  27154  fusgreg2wsp  27507  nvvcop  27773  nvex  27790  phnv  27993  sheli  28395  cheli  28413  hhssabloilem  28442  choc1  28510  shintcli  28512  chintcli  28514  shsleji  28553  pjini  28882  mayete3i  28911  dmadjop  29071  nlelshi  29243  cnlnadjeui  29260  cnlnssadj  29263  bdopadj  29265  pjimai  29359  stcl  29399  atelch  29527  fcnvgreu  29795  f1od2  29822  fcobijfs  29824  uzssico  29869  iundisj2fi  29879  nnindf  29888  eliccioo  29960  gsummptres  30105  prsdm  30281  prsrn  30282  ordtrestNEW  30288  xrge0iifcnv  30300  xrge0iifcv  30301  xrge0iifiso  30302  xrge0iifhom  30304  qqhcn  30356  esumval  30429  gsumesum  30442  esumlub  30443  esumcst  30446  esumfsup  30453  issgon  30507  elrnsiga  30510  imambfm  30645  br2base  30652  sxbrsigalem0  30654  dya2iocucvr  30667  sxbrsigalem2  30669  sxbrsigalem5  30671  sxbrsiga  30673  omssubadd  30683  sitmcl  30734  oddpwdc  30737  eulerpartlemelr  30740  eulerpartlemgvv  30759  eulerpartlemgh  30761  eulerpartlemgs2  30763  eulerpartlemn  30764  sseqf  30775  ballotlem2  30871  ballotlemfp1  30874  ballotlemfc0  30875  ballotlemfcc  30876  ballotlemfmpn  30877  ballotlemsup  30887  ballotlemfrceq  30911  signswch  30959  rpsqrtcn  30992  prodfzo03  31002  itgexpif  31005  bnj1533  31240  bnj1137  31381  bnj1286  31405  bnj1408  31422  bnj1417  31427  subfacp1lem5  31484  cvmsi  31565  mpst123  31755  mpstrcl  31756  msrrcl  31758  elmsta  31763  msubvrs  31775  elmpps  31788  elmthm  31791  bcprod  31941  dfon2lem4  32006  pprodss4v  32307  ivthALT  32646  neibastop2lem  32671  nnssi2  32766  nnssi3  32767  bj-sngltagi  33275  bj-elid  33396  bj-elid2  33397  bj-cmnssmndel  33449  bj-ablssgrpel  33451  bj-ablsscmnel  33453  bj-vecssmodel  33456  bj-rrvecssvecel  33463  bj-rrvecsscmnel  33465  taupilemrplb  33478  icorempt2  33510  elxp8  33530  sin2h  33707  cos2h  33708  tan2h  33709  poimirlem14  33731  poimirlem26  33743  poimirlem27  33744  poimirlem31  33748  poimirlem32  33749  mblfinlem1  33754  cnambfre  33765  dvtan  33767  itg2addnc  33771  itg2gt0cn  33772  ftc1cnnc  33791  ftc2nc  33801  dvasin  33803  dvacos  33804  cover2  33815  sstotbnd2  33879  heibor1lem  33914  heiborlem10  33925  opidonOLD  33957  exidcl  33981  rngosn3  34029  flddivrng  34104  toycom  34748  osumcllem7N  35737  pexmidlem4N  35748  diaintclN  36833  dibintclN  36942  mapd1o  37423  hdmapevec  37610  elrfi  37753  elrfirn  37754  elrfirn2  37755  mrefg3  37767  diophin  37832  diophun  37833  eq0rabdioph  37836  eqrabdioph  37837  pellex  37895  rmxycomplete  37977  jm2.23  38058  aomclem2  38120  fglmod  38138  lsmfgcl  38139  lmhmfgima  38149  lmhmfgsplit  38151  isnumbasabl  38171  dgrsub2  38200  itgocn  38229  acsfn1p  38264  areaquad  38296  elmapintrab  38376  corcltrcl  38525  k0004val0  38946  radcnvrat  39007  uzmptshftfval  39039  binomcxplemdvsum  39048  binomcxplemnotnn0  39049  onfrALTlem2  39253  onfrALTlem2VD  39613  uzwo4  39708  disjinfi  39863  uzublem  40130  eliccelioc  40222  elicores  40234  sqrlearg  40254  fsumiunss  40281  limcdm0  40324  sumnnodd  40336  fnlimfvre  40380  limsupubuzlem  40418  limsupmnflem  40426  limsupre3uzlem  40441  climuzlem  40449  cncfshift  40561  cncfperiod  40566  icccncfext  40574  dvnprodlem1  40635  dvnprodlem2  40636  itgsin0pilem1  40639  itgsinexplem1  40643  itgsinexp  40644  ditgeqiooicc  40649  itgsubsticclem  40664  itgioocnicc  40666  itgsbtaddcnst  40671  stoweidlem34  40724  stoweidlem41  40731  stoweidlem51  40741  wallispilem2  40756  stirlinglem11  40774  dirkercncflem2  40794  fourierdlem5  40802  fourierdlem9  40806  fourierdlem17  40814  fourierdlem18  40815  fourierdlem20  40817  fourierdlem39  40836  fourierdlem48  40844  fourierdlem49  40845  fourierdlem62  40858  fourierdlem66  40862  fourierdlem68  40864  fourierdlem72  40868  fourierdlem73  40869  fourierdlem81  40877  fourierdlem83  40879  fourierdlem85  40881  fourierdlem87  40883  fourierdlem88  40884  fourierdlem92  40888  fourierdlem95  40891  fourierdlem103  40899  fourierdlem104  40900  fourierdlem112  40908  sqwvfoura  40918  sqwvfourb  40919  fouriersw  40921  etransclem24  40948  etransclem35  40959  etransclem37  40961  salexct  41025  salgencntex  41034  sge0resplit  41096  sge0split  41099  meaiuninclem  41170  caratheodorylem1  41216  volicorescl  41243  hoidmv1lelem3  41283  opnvonmbllem2  41323  ovolval2  41334  ovolval3  41337  ovolval4lem1  41339  ovolval4lem2  41340  pimiooltgt  41397  sssmf  41423  smfaddlem1  41447  smflimlem2  41456  smfrec  41472  smfdiv  41480  smfsuplem1  41493  smfsuplem3  41495  pfxfv0  41969  pfxfvlsw  41972  bgoldbtbndlem2  42263  bgoldbtbndlem3  42264  bgoldbtbnd  42266  spr0el  42294  fldhmsubc  42646  fldhmsubcALTV  42664  setrec2lem1  43002