MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sselda Unicode version

Theorem sselda 3182
Description: Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)
Hypothesis
Ref Expression
sseld.1  |-  ( ph  ->  A  C_  B )
Assertion
Ref Expression
sselda  |-  ( (
ph  /\  C  e.  A )  ->  C  e.  B )

Proof of Theorem sselda
StepHypRef Expression
1 sseld.1 . . 3  |-  ( ph  ->  A  C_  B )
21sseld 3181 . 2  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
32imp 420 1  |-  ( (
ph  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1685    C_ wss 3154
This theorem is referenced by:  elrel  4789  ffvresb  5652  1stdm  6129  oeeulem  6595  swoso  6687  erinxp  6729  boxcutc  6855  fundmen  6930  suplub2  7208  supisolem  7217  ordiso2  7226  ordtypelem2  7230  ordtypelem6  7234  ordtypelem7  7235  cantnflt  7369  cantnflem1c  7385  cantnflem1d  7386  cantnflem1  7387  cantnflem3  7389  cantnf  7391  cnfcomlem  7398  cnfcom3lem  7402  rankelb  7492  rankval3b  7494  ackbij2lem1  7841  ackbij1lem9  7850  ackbij1lem10  7851  ackbij1lem18  7859  ackbij2lem3  7863  ackbij2  7865  fin23lem7  7938  enfin2i  7943  isf32lem9  7983  isf34lem4  7999  fin1a2lem11  8032  hsmexlem4  8051  ttukeylem6  8137  fpwwe2lem8  8255  fpwwe2lem9  8256  fpwwe2  8261  canth4  8265  intwun  8353  wuncval2  8365  inttsk  8392  rankcf  8395  r1tskina  8400  tskuni  8401  elprnq  8611  suprub  9711  suprleub  9714  supmul1  9715  supmullem1  9716  supmul  9718  infmrgelb  9730  un0addcl  9993  un0mulcl  9994  suprzcl  10087  zsupss  10303  supxrleub  10640  supxrre  10641  supxrss  10646  infmxrgelb  10648  infmxrre  10649  icoshftf1o  10754  uzindi  11038  seqcl  11061  seqfveq  11065  monoord2  11072  sermono  11073  seqsplit  11074  seqcaopr2  11077  seqf1olem2a  11079  seqf1olem2  11081  seqhomo  11088  seqz  11089  seqcoll  11396  seqcoll2  11397  ccatval1  11426  ccatass  11431  revccat  11479  rexanre  11825  rexuzre  11831  rexico  11832  limsupgle  11946  limsupval2  11949  limsupgre  11950  limsupbnd2  11952  rlim2lt  11966  rlim3  11967  ello12  11985  lo1bdd2  11993  elo12  11996  rlimclim1  12014  climrlim2  12016  lo1resb  12033  o1resb  12035  rlimcn2  12059  o1of2  12081  rlimsqzlem  12117  isercolllem3  12135  isercoll2  12137  climsup  12138  iseraltlem2  12150  summolem2a  12183  sumss  12192  fsumss  12193  fsumcvg3  12197  fsumsplit  12207  fsum2dlem  12228  fsum0diag2  12240  fsumless  12249  fsumabs  12254  fsumtscopo  12255  fsumparts  12259  fsumrlim  12264  fsumo1  12265  o1fsum  12266  fsumiun  12274  hashuni  12278  hashuniOLD  12279  ackbijnn  12281  binom1dif  12286  incexclem  12290  isumsplit  12294  isumrpcl  12297  isumless  12299  isumltss  12302  supcvg  12309  cvgrat  12334  mertenslem1  12335  rpnnen2  12499  bitsinv2  12629  bitsf1ocnv  12630  bitsinvp1  12635  eulerthlem2  12845  4sqlem11  12997  vdwlem6  13028  ramval  13050  ramcl2lem  13051  restid2  13330  mress  13490  mremre  13501  mreacs  13555  fullsubc  13719  subsubc  13722  funcres  13765  fuciso  13844  setcmon  13914  setcepi  13915  catccatid  13929  drsdirfi  14067  clatglbss  14226  ipodrsfi  14261  isacs3lem  14264  mrelatglb  14282  mrelatlub  14284  issubmnd  14396  gsumress  14449  gsumwspan  14463  frmdsssubm  14478  frmdss2  14480  subginv  14623  issubg2  14631  issubg4  14633  ssnmz  14654  lagsubg2  14673  resghm  14694  conjnmz  14711  conjnmzb  14712  subgga  14749  gass  14750  gasubg  14751  cntzsubm  14806  cntzmhm  14809  submod  14875  sylow1lem2  14905  sylow1lem3  14906  sylow1lem4  14907  sylow2alem2  14924  sylow2a  14925  sylow2blem2  14927  sylow3lem1  14933  sylow3lem6  14938  lsmssv  14949  lsmub2x  14953  lsmelvalm  14957  lsmcom2  14961  pj1lid  15005  pj1rid  15006  efgrelexlemb  15054  frgpup1  15079  frgpup3lem  15081  cntzcmn  15131  gsumval3eu  15185  gsumval3  15186  gsumzaddlem  15198  gsumzoppg  15211  dprdfadd  15250  dprdres  15258  dprdcntz2  15268  dprddisj2  15269  dprd2dlem1  15271  dmdprdsplit2lem  15275  ablfac1lem  15298  ablfac1b  15300  ablfac1c  15301  ablfac1eu  15303  pgpfac1lem1  15304  pgpfac1lem2  15305  pgpfac1lem3  15307  pgpfac1lem4  15308  ablfaclem3  15317  rngidss  15362  invrpropd  15475  subrg1  15550  subrginv  15556  subrgunit  15558  cntzsubr  15572  abvres  15599  lssel  15690  islss3  15711  lssintcl  15716  lmhmima  15799  lmhmpreima  15800  lbsel  15826  lbspropd  15847  lsmcv  15889  lspsolvlem  15890  lbsextlem2  15907  lidlsubcl  15963  drngnidl  15976  issubassa2  16079  mplcoe1  16204  mplcoe2  16206  subrgascl  16234  subrgasclcl  16235  zlpirlem1  16436  ocvocv  16566  ocvlss  16567  pjfo  16610  ocvpj  16612  obsne0  16620  obselocv  16623  tgclb  16703  tgidm  16713  pptbas  16740  toponmre  16825  clslp  16874  tgrest  16885  perfopn  16910  ordtbas  16917  ordtrest2lem  16928  pnrmcld  17065  ist1-3  17072  isreg2  17100  cncmp  17114  cmpsublem  17121  tgcmp  17123  cmpcld  17124  hauscmplem  17128  2ndcomap  17179  1stcelcls  17182  restlly  17204  lly1stc  17217  kgentopon  17228  llycmpkgen2  17240  txcls  17294  ptclsg  17304  txcnp  17309  txdis1cn  17324  txcmplem1  17330  txkgen  17341  xkoptsub  17343  xkopt  17344  xkococnlem  17348  xkoinjcn  17376  basqtop  17397  tgqtop  17398  kqfvima  17416  kqreglem1  17427  fbelss  17523  fbssfi  17527  fgabs  17569  trfg  17581  uffixfr  17613  uffixsn  17615  elfm2  17638  fmfnfmlem4  17647  fmfnfm  17648  flimnei  17657  flimrest  17673  flimcls  17675  flimsncls  17676  flffbas  17685  fclsrest  17714  fclscmp  17720  alexsublem  17733  ptcmplem3  17743  ptcmplem4  17744  subgntr  17784  opnsubg  17785  clssubg  17786  tgpconcomp  17790  divstgpopn  17797  divstgplem  17798  tsmssubm  17820  tgptsmscls  17827  tgptsmscld  17828  tsmsxplem1  17830  tsmsxplem2  17831  imasdsf1olem  17932  blpnfctr  17977  xmetresbl  17978  mopni2  18034  mopni3  18035  rnblopn  18040  tgioo  18297  xrsmopn  18313  zdis  18317  icccmplem3  18324  reconnlem2  18327  opnreen  18331  metdsf  18347  metdsge  18348  metdsle  18351  metdsre  18352  metnrmlem2  18359  metnrmlem3  18360  fsumcn  18369  climcncf  18399  icccvx  18443  cnheibor  18448  bndth  18451  lebnumlem1  18454  lebnumlem2  18455  pi1grplem  18542  clmneg  18574  nmoleub2lem3  18591  cphsqrcl  18615  cphabscl  18616  clsocv  18672  iscfil2  18687  cfil3i  18690  cfilfcls  18695  cmetcaulem  18709  iscmet3lem2  18713  cfilresi  18716  caussi  18718  lmclim  18723  minveclem1  18783  minveclem3b  18787  minveclem4  18791  minveclem6  18793  pjthlem2  18797  ivth2  18810  ivthicc  18813  ovollb2lem  18842  ovoliunlem1  18856  ovolicc2lem4  18874  ioombl1lem4  18913  dyadmax  18948  dyadmbl  18950  opnmbllem  18951  volsup2  18955  volivth  18957  vitalilem5  18962  i1fima  19028  i1fd  19031  itg1val2  19034  itg1cl  19035  itg1ge0  19036  itg11  19041  i1fadd  19045  i1fmul  19046  itg1addlem4  19049  itg1addlem5  19050  i1fmulc  19053  itg1mulc  19054  itg10a  19060  itg1ge0a  19061  itg1climres  19064  mbfi1fseqlem4  19068  mbfi1fseqlem5  19069  mbfi1flim  19073  mbfmullem2  19074  itg2const2  19091  itg2splitlem  19098  itg2split  19099  itg2gt0  19110  itg2cnlem2  19112  iblss  19154  iblss2  19155  itgss3  19164  itgless  19166  itgfsum  19176  itgsplit  19185  itgsplitioo  19187  itggt0  19191  itgcn  19192  ditgcl  19203  ditgswap  19204  ditgsplitlem  19205  ellimc3  19224  perfdvf  19248  dvreslem  19254  dvcnp  19263  dvcnp2  19264  dvaddbr  19282  dvmulbr  19283  dvcjbr  19293  dvmptfsum  19317  dvcnvlem  19318  dvlip  19335  dvlipcn  19336  dvlip2  19337  dv11cn  19343  dvivthlem1  19350  dvivthlem2  19351  dvne0  19353  lhop1lem  19355  lhop2  19357  lhop  19358  dvcvx  19362  dvfsumle  19363  dvfsumge  19364  dvfsumabs  19365  dvfsumlem2  19369  dvfsumlem3  19370  dvfsumrlimge0  19372  dvfsumrlim2  19374  ftc1lem1  19377  ftc1lem4  19381  ftc1lem6  19383  itgsubstlem  19390  ig1peu  19552  plyeq0lem  19587  plypf1  19589  coeeulem  19601  vieta1lem1  19685  vieta1lem2  19686  plyexmo  19688  aaliou3lem2  19718  taylthlem1  19747  taylthlem2  19748  ulmdvlem1  19772  ulmdvlem3  19774  mtest  19776  radcnv0  19787  pserulm  19793  psercnlem2  19795  psercnlem1  19796  psercn  19797  pserdvlem1  19798  pserdvlem2  19799  pserdv  19800  pserdv2  19801  abelthlem3  19804  abelthlem4  19805  abelthlem9  19811  pige3  19880  efif1olem4  19902  efopnlem2  19999  efopn  20000  logccv  20005  loglesqr  20093  rlimcnp  20255  rlimcnp2  20256  xrlimcnp  20258  efrlim  20259  jensenlem1  20276  jensenlem2  20277  jensen  20278  fsumharmonic  20300  wilthlem2  20302  basellem3  20315  basellem5  20317  chtdif  20391  sqff1o  20415  musumsum  20427  muinv  20428  chtublem  20445  fsumvma  20447  vmasum  20450  chpval2  20452  chpchtsum  20453  chpub  20454  perfectlem2  20464  lgsquadlem2  20589  chebbnd1lem1  20613  dchrisumlem2  20634  dchrisumlem3  20635  dchrmusum2  20638  dchrisum0fno1  20655  rpvmasum2  20656  dchrisum0lem1b  20659  dchrisum0lem1  20660  rplogsum  20671  mudivsum  20674  mulogsum  20676  mulog2sumlem2  20679  selberg2lem  20694  chpdifbndlem1  20697  pntrlog2bndlem6  20727  pntrlog2bnd  20728  pntlemj  20747  pntlemf  20749  pntlem3  20753  subgoinv  20968  ubthlem1  21442  ubthlem2  21443  ubthlem3  21444  minvecolem1  21446  minvecolem4  21452  minvecolem5  21453  minvecolem6  21454  shel  21783  chel  21803  ocorth  21863  pjpreeq  21970  chscllem1  22209  chscllem2  22210  spansncvi  22224  ballotlemsel1i  23065  ballotlemfrceq  23081  erdszelem8  23134  cvmscld  23209  cvmsss2  23210  cvmopnlem  23214  cvmlift2lem9  23247  cvmlift2lem11  23249  cvmlift2lem12  23250  cvmliftpht  23254  umgraex  23280  eupares  23304  dedekind  23486  trpredelss  23637  sltres  23719  axfelem9  23756  axfelem10  23757  axlowdimlem13  23990  axlowdimlem16  23993  axcontlem4  24003  axcontlem10  24009  bpolycl  24195  bpolysum  24196  bpolydiflem  24197  iscst4  24577  altretop  25000  lvsovso  25026  lvsovso2  25027  supnuf  25029  idsubfun  25258  vtarsuelt  25295  morexcmp  25367  opnrebl2  25636  fnessex  25675  fneuni  25676  comppfsc  25707  neibastop1  25708  neibastop2lem  25709  neibastop3  25711  sdclem1  25853  mettrifi  25873  sstotbnd2  25898  equivtotbnd  25902  isbndx  25906  totbndbnd  25913  equivbnd2  25916  cntotbnd  25920  heibor1lem  25933  heiborlem3  25937  heibor  25945  iccbnd  25964  idlcl  26042  divrngidl  26053  ismrcd1  26173  mzpf  26214  mzpindd  26224  fphpdo  26300  pell14qrre  26342  pell14qrne0  26343  elpell14qr2  26347  elpell1qr2  26357  pellfundex  26371  dnnumch3lem  26543  dnnumch3  26544  fnwe2lem2  26548  aomclem4  26554  kelac1  26561  kercvrlsm  26581  dsmmsubg  26609  frlmsslsp  26648  hbtlem2  26728  hbtlem5  26732  flcidc  26779  f1omvdmvd  26786  f1omvdconj  26789  symggen  26811  psgnunilem5  26817  psgnunilem2  26818  cntzsdrg  26910  climinf  27132  stoweidlem18  27167  stoweidlem26  27175  stoweidlem27  27176  stoweidlem31  27180  stoweidlem35  27184  stoweidlem39  27188  stoweidlem42  27191  stoweidlem48  27197  stoweidlem51  27200  stoweidlem56  27205  stoweidlem61  27210  bnj1137  28293  bnj1498  28359  lsatfixedN  28467  elpaddn0  29257  diaintclN  30516  dibglbN  30624  dibintclN  30625  dihrnlss  30735  dihglblem3N  30753  dihglblem6  30798  dihintcl  30802  dochkr1  30936  dochkr1OLDN  30937  lcfrlem5  31004  lcfr  31043  mapdrvallem2  31103  hgmapvvlem3  31386  hdmapoc  31392  hlhilocv  31418
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator