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

Theorem sseli 3632
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
StepHypRef Expression
1 sseli.1 . 2 𝐴𝐵
2 ssel 3630 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  sselii  3633  sseldi  3634  elun1  3813  elun2  3814  elopabran  5043  copsex2ga  5264  issref  5544  2elresin  6040  nfvres  6262  fvco4i  6315  mptrcl  6328  fvmptss  6331  fvmptex  6333  fvmptnf  6341  elfvmptrab1  6344  fvopab4ndm  6346  fvimacnvi  6371  elpreima  6377  iinpreima  6385  ofrfval  6947  ofval  6948  off  6954  nnon  7113  finds  7134  finds2  7136  offres  7205  eqopi  7246  op1steq  7254  dfoprab4  7269  bropopvvv  7300  bropfvvvv  7302  curry1val  7315  curry2val  7319  reldmtpos  7405  wfrlem4  7463  wfrlem10  7469  smores3  7495  smores2  7496  frsuc  7577  nnfi  8194  unifpw  8310  f1opwfi  8311  fival  8359  fi0  8367  dffi2  8370  elfiun  8377  cantnfp1lem1  8613  cantnfp1lem3  8615  epfrs  8645  r1fin  8674  r1tr  8677  r1ordg  8679  r1ord3g  8680  r1val1  8687  tz9.12lem3  8690  tcrank  8785  cplem1  8790  hta  8798  tskwe  8814  cardprclem  8843  r0weon  8873  fodomfi2  8921  alephfplem3  8967  dfac12r  9006  ackbij1lem6  9085  ackbij1lem9  9088  ackbij1lem10  9089  ackbij1lem11  9090  ackbij1lem16  9095  ackbij1lem18  9097  ackbij2  9103  fin23lem24  9182  fin23lem26  9185  fin23lem28  9200  fin23lem30  9202  fin23lem31  9203  isfin1-3  9246  fin1a2lem6  9265  hsmexlem4  9289  hsmexlem5  9290  hsmexlem6  9291  axdc2lem  9308  axdc3lem2  9311  axcclem  9317  ac6num  9339  brdom5  9389  brdom4  9390  canthp1lem2  9513  r1tskina  9642  gruina  9678  grur1a  9679  pinn  9738  0nnq  9784  elpqn  9785  recn  10064  rexr  10123  dedekindle  10239  ltord1  10592  leord1  10593  eqord1  10594  nnre  11065  nncn  11066  nnind  11076  nnnn0  11337  nn0re  11339  nn0cn  11340  nn0xnn0  11405  nnz  11437  nn0z  11438  nnq  11839  qcn  11840  rpre  11877  xrge0nre  12315  difreicc  12342  iccshftri  12345  iccshftli  12347  iccdili  12349  icccntri  12351  fzval2  12367  fzelp1  12431  4fvwrd4  12498  elfzo1  12557  ico01fl0  12660  expcllem  12911  expcl2lem  12912  m1expcl2  12922  bcm1k  13142  bcpasc  13148  hashbclem  13274  swrd0fv0  13486  swrd0fvlsw  13489  cshimadifsn  13621  sqrlem5  14031  cau3lem  14138  caubnd  14142  climconst2  14323  rlimres  14333  lo1res  14334  lo1resb  14339  rlimresb  14340  o1resb  14341  o1of2  14387  o1rlimmul  14393  caurcvg  14451  caucvg  14453  ackbijnn  14604  binomlem  14605  incexclem  14612  divcnvshft  14631  zprod  14711  fprodge1  14770  risefaccllem  14788  fallfaccllem  14789  bpolydiflem  14829  bpoly4  14834  dvdsflip  15086  divalglem8  15170  sadadd  15236  smueqlem  15259  smumul  15262  isprm3  15443  phimullem  15531  prmdiveq  15538  unbenlem  15659  prmrec  15673  vdwnnlem1  15746  vdwnnlem3  15748  ramtcl2  15762  prmgaplem4  15805  cshwshashlem1  15849  isstruct2  15914  structcnvcnv  15918  fvsetsid  15937  strlemor1OLD  16016  imasdsval2  16223  xpsfrnel2  16272  mreunirn  16308  mrcfval  16315  mrisval  16337  isacs2  16361  acsfn  16367  arwval  16740  coafval  16761  coapm  16768  isdrs2  16986  isacs3lem  17213  psssdm2  17262  tsrss  17270  submnd0  17367  nmzsubg  17682  nmznsg  17685  resscntz  17810  cntzmhm  17817  symgtrinv  17938  pmtrdifellem4  17945  psgnpmtr  17976  efginvrel2  18186  efginvrel1  18187  efgsp1  18196  efgsres  18197  efgsfo  18198  frgpinv  18223  frgpupf  18232  frgpup1  18234  subcmn  18288  torsubg  18303  dprd2dlem1  18486  dpjidcl  18503  ablfaclem3  18532  subrgpropd  18862  lssacs  19015  sralmod  19235  psrbaglefi  19420  mplsubglem  19482  ressmpladd  19505  ressmplmul  19506  ressmplvsca  19507  mplmonmul  19512  mplind  19550  ply1bascl  19621  cnsubdrglem  19845  rege0subm  19850  rge0srg  19865  zringunit  19884  znrrg  19962  psgnghm  19974  zrhpsgnevpm  19985  evpmodpmf1o  19990  pmtrodpm  19991  frlmsslsp  20183  islinds4  20222  lmimlbs  20223  lbslcic  20228  mdetralt  20462  mdetunilem7  20472  chfacfpmmulgsum2  20718  basdif0  20805  tgval2  20808  mreclatdemoBAD  20948  ordtbas  21044  ordtrest  21054  ordtrestixx  21074  fincmp  21244  cmpfi  21259  bwth  21261  iunconn  21279  1stcrest  21304  hauslly  21343  kgentop  21393  ptbasin  21428  ptcnplem  21472  infil  21714  filunirn  21733  uzrest  21748  elflim  21822  hauspwpwf1  21838  flffval  21840  fclsval  21859  isfcls  21860  fcfval  21884  alexsubALTlem3  21900  alexsubALTlem4  21901  ustn0  22071  fmucndlem  22142  xmetunirn  22189  blbas  22282  blres  22283  mopnval  22290  setsmstopn  22330  tmsval  22333  tngtopn  22501  qtopbaslem  22609  xrtgioo  22656  reperflem  22668  icccmplem1  22672  reconnlem2  22677  xrge0tsms  22684  icopnfhmeo  22789  icccvx  22796  bndth  22804  reparphti  22843  pcofval  22856  pcoval1  22859  pcoval2  22862  pcoass  22870  pcorevlem  22872  pcorev2  22874  pi1xfrcnv  22903  nmhmcn  22966  csscld  23094  cfilfval  23108  caufval  23119  cfilres  23140  bcthlem1  23167  ivthlem1  23266  ivthlem3  23268  ovolicc2lem3  23333  ovolicc2lem4  23334  ioombl1lem4  23375  vitalilem1  23422  mbflimsup  23478  i1fima2  23491  i1fd  23493  i1f0  23499  i1f1  23502  itg1addlem4  23511  itg1addlem5  23512  iblmbf  23579  ellimc2  23686  limcres  23695  limcun  23704  dvbsss  23711  perfdvf  23712  dvres2lem  23719  dvaddbr  23746  rolle  23798  cmvth  23799  dvlip  23801  dvlipcn  23802  dvle  23815  lhop1lem  23821  dvfsumle  23829  dvfsumge  23830  dvfsumabs  23831  dvfsumlem2  23835  ftc2  23852  itgparts  23855  itgsubstlem  23856  itgsubst  23857  deg1mul3  23920  coeval  24024  coeeu  24026  dgrval  24029  coef3  24033  coemulc  24056  dgrsub  24073  coecj  24079  dvply2  24086  dvnply  24088  quotval  24092  fta1  24108  plyexmo  24113  aacjcl  24127  taylfval  24158  dvtaylp  24169  abelth  24240  pilem2  24251  pilem3  24252  sinord  24325  recosf1o  24326  resinf1o  24327  tanord1  24328  eff1olem  24339  dvloglem  24439  dvlog  24442  dvlog2lem  24443  advlogexp  24446  logtayl  24451  logtayl2  24453  dvcncxp1  24529  dvcnsqrt  24530  cxpcn3lem  24533  cxpcn3  24534  sqrtcn  24536  loglesqrt  24544  1cubr  24614  acosrecl  24675  rlimcnp2  24738  xrlimcnp  24740  efrlim  24741  jensen  24760  lgamgulmlem2  24801  lgamucov2  24810  basellem4  24855  ppiprm  24922  chtprm  24924  prmorcht  24949  musum  24962  chpchtsum  24989  dchrinvcl  25023  dchrghm  25026  dchrinv  25031  dchrsum2  25038  dchrsum  25039  rplogsumlem2  25219  rpvmasumlem  25221  dchrisum0lem2a  25251  dirith2  25262  pnt  25348  tglng  25486  axlowdimlem6  25872  axlowdimlem16  25882  axlowdimlem17  25883  axlowdim  25886  axeuclidlem  25887  axcontlem2  25890  axcontlem7  25895  axcontlem8  25896  nbusgrvtxm1uvtx  26356  wlk1walk  26591  pthdivtx  26681  pthdadjvtx  26682  crctcshwlkn0lem2  26759  crctcshwlkn0lem4  26761  clwwisshclwws  26972  fusgreg2wsp  27316  nvvcop  27577  nvex  27594  phnv  27797  sheli  28199  cheli  28217  hhssabloilem  28246  choc1  28314  shintcli  28316  chintcli  28318  shsleji  28357  pjini  28686  mayete3i  28715  dmadjop  28875  nlelshi  29047  cnlnadjeui  29064  cnlnssadj  29067  bdopadj  29069  pjimai  29163  stcl  29203  atelch  29331  fcnvgreu  29600  f1od2  29627  fcobijfs  29629  xrge0infss  29653  uzssico  29674  iundisj2fi  29684  nnindf  29693  eliccioo  29767  xrge0mulgnn0  29817  xrge0omnd  29839  gsummptres  29912  prsdm  30088  prsrn  30089  ordtrestNEW  30095  xrge0iifcnv  30107  xrge0iifcv  30108  xrge0iifiso  30109  xrge0iifhom  30111  qqhcn  30163  esumval  30236  gsumesum  30249  esumlub  30250  esumcst  30253  esumfsup  30260  esumcvgre  30281  issgon  30314  elrnsiga  30317  imambfm  30452  br2base  30459  sxbrsigalem0  30461  dya2iocucvr  30474  sxbrsigalem2  30476  sxbrsigalem5  30478  sxbrsiga  30480  omssubadd  30490  sitmcl  30541  oddpwdc  30544  eulerpartlemelr  30547  eulerpartlemgvv  30566  eulerpartlemgh  30568  eulerpartlemgs2  30570  eulerpartlemn  30571  sseqf  30582  ballotlem2  30678  ballotlemfp1  30681  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemfmpn  30684  ballotlemsup  30694  ballotlemfrceq  30718  signswch  30766  rpsqrtcn  30799  prodfzo03  30809  itgexpif  30812  bnj1533  31048  bnj1137  31189  bnj1286  31213  bnj1408  31230  bnj1417  31235  subfacp1lem5  31292  cvmsi  31373  mpst123  31563  mpstrcl  31564  msrrcl  31566  elmsta  31571  msubvrs  31583  elmpps  31596  elmthm  31599  bcprod  31750  dfon2lem4  31815  pprodss4v  32116  ivthALT  32455  neibastop2lem  32480  nnssi2  32579  nnssi3  32580  bj-sngltagi  33095  bj-elid  33215  bj-elid2  33216  bj-cmnssmndel  33267  bj-ablssgrpel  33269  bj-ablsscmnel  33271  bj-vecssmodel  33274  bj-rrvecssvecel  33281  bj-rrvecsscmnel  33283  taupilemrplb  33296  icorempt2  33329  elxp8  33349  sin2h  33529  cos2h  33530  tan2h  33531  poimirlem14  33553  poimirlem26  33565  poimirlem27  33566  poimirlem31  33570  poimirlem32  33571  mblfinlem1  33576  cnambfre  33588  dvtan  33590  itg2addnc  33594  itg2gt0cn  33595  ftc1cnnc  33614  ftc2nc  33624  dvasin  33626  dvacos  33627  cover2  33638  sstotbnd2  33703  heibor1lem  33738  heiborlem10  33749  opidonOLD  33781  exidcl  33805  rngosn3  33853  flddivrng  33928  toycom  34578  osumcllem7N  35566  pexmidlem4N  35577  diaintclN  36664  dibintclN  36773  mapd1o  37254  hdmapevec  37444  elrfi  37574  elrfirn  37575  elrfirn2  37576  mrefg3  37588  diophin  37653  diophun  37654  eq0rabdioph  37657  eqrabdioph  37658  pellex  37716  rmxycomplete  37799  jm2.23  37880  aomclem2  37942  fglmod  37960  lsmfgcl  37961  lmhmfgima  37971  lmhmfgsplit  37973  isnumbasabl  37993  dgrsub2  38022  itgocn  38051  acsfn1p  38086  areaquad  38119  elmapintrab  38199  corcltrcl  38348  k0004val0  38769  radcnvrat  38830  uzmptshftfval  38862  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  onfrALTlem2  39078  onfrALTlem2VD  39439  uzwo4  39535  disjinfi  39694  uzublem  39970  eliccxr  40055  eliccelioc  40065  elicores  40078  sqrlearg  40098  fsumiunss  40125  limcdm0  40168  sumnnodd  40180  fnlimfvre  40224  limsupubuzlem  40262  limsupmnflem  40270  limsupre3uzlem  40285  climuzlem  40293  cncfshift  40405  cncfperiod  40410  icccncfext  40418  dvnprodlem1  40479  dvnprodlem2  40480  itgsin0pilem1  40483  itgsinexplem1  40487  itgsinexp  40488  ditgeqiooicc  40494  itgsubsticclem  40509  itgioocnicc  40511  itgsbtaddcnst  40516  stoweidlem34  40569  stoweidlem41  40576  stoweidlem51  40586  wallispilem2  40601  stirlinglem11  40619  dirkercncflem2  40639  fourierdlem5  40647  fourierdlem9  40651  fourierdlem17  40659  fourierdlem18  40660  fourierdlem20  40662  fourierdlem39  40681  fourierdlem48  40689  fourierdlem49  40690  fourierdlem62  40703  fourierdlem66  40707  fourierdlem68  40709  fourierdlem72  40713  fourierdlem73  40714  fourierdlem81  40722  fourierdlem83  40724  fourierdlem85  40726  fourierdlem87  40728  fourierdlem88  40729  fourierdlem92  40733  fourierdlem95  40736  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  sqwvfoura  40763  sqwvfourb  40764  fouriersw  40766  etransclem24  40793  etransclem35  40804  etransclem37  40806  salexct  40870  salgencntex  40879  gsumge0cl  40906  sge0tsms  40915  sge0resplit  40941  sge0split  40944  meaiuninclem  41015  caratheodorylem1  41061  volicorescl  41088  hoidmv1lelem3  41128  opnvonmbllem2  41168  ovolval2  41179  ovolval3  41182  ovolval4lem1  41184  ovolval4lem2  41185  pimiooltgt  41242  sssmf  41268  smfaddlem1  41292  smflimlem2  41301  smfrec  41317  smfdiv  41325  smfsuplem1  41338  smfsuplem3  41340  pfxfv0  41725  pfxfvlsw  41728  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  bgoldbtbnd  42022  spr0el  42057  fldhmsubc  42409  fldhmsubcALTV  42427  setrec2lem1  42765
  Copyright terms: Public domain W3C validator