Theorem sseli 3856

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

Syntax hints:   → wi 4   ∈ wcel 2051   ⊆ wss 3831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-in 3838  df-ss 3845

This theorem is referenced by:  sselii  3857  sseldi  3858  elun1  4043  elun2  4044  elopabran  5304  copsex2ga  5534  2elresin  6306  nfvres  6541  fvco4i  6595  mptrcl  6609  fvmptss  6612  fvmptex  6614  fvmptnf  6622  elfvmptrab1  6626  fvopab4ndm  6628  fvimacnvi  6653  elpreima  6659  iinpreima  6668  ofrfval  7241  ofval  7242  off  7248  nnon  7408  finds  7429  finds2  7431  eqopi  7543  op1steq  7551  dfoprab4  7567  bropopvvv  7599  bropfvvvv  7601  reldmtpos  7709  wfrlem4OLD  7768  wfrlem10  7774  smores2  7801  frsuc  7882  nnfi  8512  unifpw  8628  cantnfp1lem1  8941  cantnfp1lem3  8943  r1fin  9002  r1tr  9005  r1ordg  9007  r1ord3g  9008  r1val1  9015  tz9.12lem3  9018  tcrank  9113  cplem1  9118  hta  9126  tskwe  9179  cardprclem  9208  alephfplem3  9332  dfac12r  9372  ackbij1lem16  9461  ackbij2  9469  fin23lem28  9566  fin23lem30  9568  fin23lem31  9569  fin1a2lem6  9631  hsmexlem4  9655  hsmexlem5  9656  hsmexlem6  9657  axdc2lem  9674  axdc3lem2  9677  axcclem  9683  ac6num  9705  brdom5  9755  brdom4  9756  r1tskina  10008  gruina  10044  grur1a  10045  pinn  10104  0nnq  10150  elpqn  10151  recn  10431  rexr  10492  ltord1  10973  leord1  10974  eqord1  10975  nnre  11453  nncn  11454  nnind  11465  nnnn0  11721  nn0re  11723  nn0cn  11724  nn0xnn0  11789  nnz  11823  nn0z  11824  nnq  12182  qcn  12183  rpre  12218  rpreOLD  12219  eliccxr  12645  difreicc  12692  iccshftri  12695  iccshftli  12697  iccdili  12699  icccntri  12701  fzval2  12717  fzelp1  12781  4fvwrd4  12849  elfzo1  12908  ico01fl0  13010  expcllem  13261  expcl2lem  13262  m1expcl2  13272  bcm1k  13496  bcpasc  13502  hashbclem  13629  wrdv  13694  swrd0fv0OLD  13838  swrd0fvlswOLD  13841  pfxfv0  13880  pfxfvlsw  13883  cshimadifsn  14059  swrds2m  14171  sqrlem5  14473  cau3lem  14581  caubnd  14585  climconst2  14772  o1of2  14836  o1rlimmul  14842  caurcvg  14900  caucvg  14902  binomlem  15050  incexclem  15057  divcnvshft  15076  zprod  15157  fprodge1  15215  risefaccllem  15233  fallfaccllem  15234  bpolydiflem  15274  bpoly4  15279  dvdsflip  15533  divalglem8  15617  sadadd  15682  smumul  15708  isprm3  15889  phimullem  15978  prmdiveq  15985  unbenlem  16106  vdwnnlem1  16193  vdwnnlem3  16195  ramtcl2  16209  prmgaplem4  16252  cshwshashlem1  16291  structcnvcnv  16359  fvsetsid  16377  imasdsval2  16651  xpsfrnel2cda  16704  mreunirn  16742  mrcfval  16749  mrisval  16771  coapm  17201  tsrss  17703  submnd0  17800  nmzsubg  18116  nmznsg  18119  cntzmhm  18252  symgtrinv  18373  pmtrdifellem4  18380  psgnpmtr  18412  efginvrel2  18623  efginvrel1  18624  efgsp1  18633  efgsres  18634  efgsresOLD  18635  efgsfo  18636  frgpinv  18662  frgpupf  18671  frgpup1  18673  subcmn  18727  torsubg  18742  dprd2dlem1  18925  dpjidcl  18942  ablfaclem3  18971  acsfn1p  19312  lssacs  19473  psrbaglefi  19878  mplsubglem  19940  ressmpladd  19963  ressmplmul  19964  ressmplvsca  19965  mplmonmul  19970  ply1bascl  20089  cnsubdrglem  20313  rege0subm  20318  rge0srg  20333  zringunit  20352  znrrg  20429  psgnghm  20441  zrhpsgnevpm  20452  evpmodpmf1o  20457  pmtrodpm  20458  phlssphl  20520  frlmsslsp  20657  islinds4  20696  lmimlbs  20697  lbslcic  20702  mdetralt  20936  mdetunilem7  20946  chfacfpmmulgsum2  21192  tgval2  21283  ordtbas  21519  ordtrestixx  21549  hauslly  21819  kgentop  21869  ptbasin  21904  filunirn  22209  uzrest  22224  elflim  22298  flffval  22316  fclsval  22335  isfcls  22336  fcfval  22360  ustn0  22547  fmucndlem  22618  xmetunirn  22665  mopnval  22766  setsmstopn  22806  tmsval  22809  tngtopn  22977  qtopbaslem  23085  xrtgioo  23132  reperflem  23144  icccmplem1  23148  icopnfhmeo  23265  icccvx  23272  bndth  23280  reparphti  23319  pcoval1  23335  pcoval2  23338  pcoass  23346  pcorevlem  23348  pcorev2  23350  pi1xfrcnv  23379  csscld  23570  cfilfval  23585  caufval  23596  bcthlem1  23645  ivthlem1  23770  ivthlem3  23772  ovolicc2lem3  23838  ovolicc2lem4  23839  vitalilem1  23927  mbflimsup  23985  i1fd  24000  i1f0  24006  i1f1  24009  itg1addlem4  24018  itg1addlem5  24019  iblmbf  24086  ellimc2  24193  limcres  24202  limcun  24211  dvbsss  24218  perfdvf  24219  dvres2lem  24226  dvaddbr  24253  rolle  24305  cmvth  24306  dvlip  24308  dvlipcn  24309  dvle  24322  lhop1lem  24328  dvfsumle  24336  dvfsumge  24337  dvfsumabs  24338  dvfsumlem2  24342  ftc2  24359  itgparts  24362  itgsubstlem  24363  itgsubst  24364  deg1mul3  24427  coeval  24531  coeeu  24533  dgrval  24536  coef3  24540  coemulc  24563  dgrsub  24580  coecj  24586  dvply2  24593  dvnply  24595  quotval  24599  fta1  24615  plyexmo  24620  aacjcl  24634  taylfval  24665  dvtaylp  24676  abelth  24747  pilem3  24759  sinord  24834  recosf1o  24835  resinf1o  24836  tanord1  24837  eff1olem  24848  dvloglem  24947  dvlog  24950  dvlog2lem  24951  advlogexp  24954  logtayl  24959  logtayl2  24961  dvcncxp1  25040  dvcnsqrt  25041  cxpcn3lem  25044  cxpcn3  25045  sqrtcn  25047  loglesqrt  25055  1cubr  25136  acosrecl  25197  efrlim  25264  jensen  25283  lgamgulmlem2  25324  lgamucov2  25333  basellem4  25378  musum  25485  dchrinvcl  25546  dchrghm  25549  dchrinv  25554  dchrsum2  25561  dchrsum  25562  rpvmasumlem  25780  dchrisum0lem2a  25810  pnt  25907  tglng  26049  axlowdimlem6  26451  axlowdimlem16  26461  axlowdimlem17  26462  axlowdim  26465  axeuclidlem  26466  axcontlem2  26469  axcontlem7  26474  axcontlem8  26475  nbusgrvtxm1uvtx  26905  wlk1walk  27138  pthdivtx  27233  pthdadjvtx  27234  crctcshwlkn0lem2  27312  crctcshwlkn0lem4  27314  clwwisshclwws  27545  fusgreg2wsp  27885  nvvcop  28163  nvex  28180  phnv  28383  sheli  28785  cheli  28803  hhssabloilem  28832  choc1  28900  shintcli  28902  chintcli  28904  shsleji  28943  pjini  29272  mayete3i  29301  dmadjop  29461  nlelshi  29633  cnlnadjeui  29650  cnlnssadj  29653  bdopadj  29655  pjimai  29749  stcl  29789  atelch  29917  fcnvgreu  30197  f1od2  30233  fcobijfs  30235  uzssico  30283  iundisj2fi  30293  nnindf  30305  eliccioo  30377  cyc3genpm  30497  gsummptres  30561  ordtrestNEW  30840  xrge0iifcnv  30852  xrge0iifcv  30853  xrge0iifiso  30854  xrge0iifhom  30856  qqhcn  30908  esumval  30981  gsumesum  30994  esumlub  30995  esumcst  30998  esumfsup  31005  issgon  31059  elrnsiga  31062  imambfm  31197  br2base  31204  sxbrsigalem0  31206  dya2iocucvr  31219  sxbrsigalem2  31221  sxbrsigalem5  31223  sxbrsiga  31225  omssubadd  31235  sitmcl  31286  oddpwdc  31289  eulerpartlemelr  31292  eulerpartlemgvv  31311  eulerpartlemgh  31313  eulerpartlemgs2  31315  eulerpartlemn  31316  sseqf  31328  ballotlem2  31424  ballotlemfp1  31427  ballotlemfc0  31428  ballotlemfcc  31429  ballotlemfmpn  31430  ballotlemsup  31440  ballotlemfrceq  31464  signswch  31509  rpsqrtcn  31544  prodfzo03  31554  itgexpif  31557  bnj1533  31803  bnj1137  31944  bnj1286  31968  bnj1408  31985  bnj1417  31990  subfacp1lem5  32056  cvmsi  32137  mpst123  32347  mpstrcl  32348  msrrcl  32350  elmsta  32355  msubvrs  32367  elmpps  32380  elmthm  32383  bcprod  32530  dfon2lem4  32591  pprodss4v  32906  ivthALT  33244  neibastop2lem  33269  nnssi2  33363  nnssi3  33364  bj-sngltagi  33852  bj-elid  33978  bj-elid2  33979  bj-fvmptunsn1  34048  bj-cmnssmndel  34060  bj-ablssgrpel  34062  bj-ablsscmnel  34064  bj-vecssmodel  34067  bj-rrvecssvecel  34074  bj-rrvecsscmnel  34076  taupilemrplb  34083  icorempo  34114  elxp8  34134  sin2h  34363  cos2h  34364  tan2h  34365  poimirlem14  34387  poimirlem26  34399  poimirlem27  34400  poimirlem31  34404  poimirlem32  34405  mblfinlem1  34410  cnambfre  34421  dvtan  34423  itg2addnc  34427  itg2gt0cn  34428  ftc1cnnc  34447  ftc2nc  34457  dvasin  34459  dvacos  34460  cover2  34471  sstotbnd2  34534  heibor1lem  34569  heiborlem10  34580  opidonOLD  34612  exidcl  34636  rngosn3  34684  flddivrng  34759  toycom  35594  osumcllem7N  36583  pexmidlem4N  36594  diaintclN  37679  dibintclN  37788  mapd1o  38269  hdmapevec  38456  prjspvs  38708  prjspeclsp  38710  0prjspnrel  38717  elrfi  38727  elrfirn  38728  elrfirn2  38729  mrefg3  38741  diophin  38806  diophun  38807  eq0rabdioph  38810  eqrabdioph  38811  pellex  38869  rmxycomplete  38951  jm2.23  39030  aomclem2  39092  fglmod  39110  lsmfgcl  39111  lmhmfgima  39121  lmhmfgsplit  39123  isnumbasabl  39143  dgrsub2  39172  itgocn  39201  areaquad  39260  elmapintrab  39339  corcltrcl  39488  k0004val0  39908  elscottab  39996  radcnvrat  40103  uzmptshftfval  40135  binomcxplemdvsum  40144  binomcxplemnotnn0  40145  onfrALTlem2  40339  onfrALTlem2VD  40682  uzwo4  40774  disjinfi  40915  mptssid  40974  uzublem  41170  eliccelioc  41263  elicores  41275  sqrlearg  41295  fsumiunss  41322  limcdm0  41365  sumnnodd  41377  fnlimfvre  41421  limsupubuzlem  41459  limsupmnflem  41467  limsupre3uzlem  41482  climuzlem  41490  cncfshift  41622  cncfperiod  41627  icccncfext  41635  dvnprodlem1  41696  dvnprodlem2  41697  itgsin0pilem1  41700  itgsinexplem1  41704  itgsinexp  41705  ditgeqiooicc  41710  itgsubsticclem  41725  itgioocnicc  41727  itgsbtaddcnst  41732  stoweidlem34  41785  stoweidlem41  41792  stoweidlem51  41802  wallispilem2  41817  stirlinglem11  41835  dirkercncflem2  41855  fourierdlem5  41863  fourierdlem9  41867  fourierdlem17  41875  fourierdlem18  41876  fourierdlem20  41878  fourierdlem39  41897  fourierdlem48  41905  fourierdlem49  41906  fourierdlem62  41919  fourierdlem66  41923  fourierdlem68  41925  fourierdlem72  41929  fourierdlem73  41930  fourierdlem81  41938  fourierdlem83  41940  fourierdlem85  41942  fourierdlem87  41944  fourierdlem88  41945  fourierdlem92  41949  fourierdlem95  41952  fourierdlem103  41960  fourierdlem104  41961  fourierdlem112  41969  sqwvfoura  41979  sqwvfourb  41980  fouriersw  41982  etransclem24  42009  etransclem35  42020  etransclem37  42022  salexct  42083  salgencntex  42092  sge0resplit  42154  sge0split  42157  meaiuninclem  42228  caratheodorylem1  42274  volicorescl  42301  hoidmv1lelem3  42341  opnvonmbllem2  42381  ovolval2  42392  ovolval3  42395  ovolval4lem1  42397  ovolval4lem2  42398  pimiooltgt  42455  sssmf  42481  smfaddlem1  42505  smflimlem2  42514  smfrec  42530  smfdiv  42538  smfsuplem1  42551  smfsuplem3  42553  spr0el  43047  bgoldbtbndlem2  43374  bgoldbtbndlem3  43375  bgoldbtbnd  43377  fldhmsubc  43754  fldhmsubcALTV  43772  setrec2lem1  44198