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

Theorem ssrdv 3438
Description: Deduction rule based on subclass definition. (Contributed by NM, 15-Nov-1995.)
Hypothesis
Ref Expression
ssrdv.1  |-  ( ph  ->  ( x  e.  A  ->  x  e.  B ) )
Assertion
Ref Expression
ssrdv  |-  ( ph  ->  A  C_  B )
Distinct variable groups:    x, A    x, B    ph, x

Proof of Theorem ssrdv
StepHypRef Expression
1 ssrdv.1 . . 3  |-  ( ph  ->  ( x  e.  A  ->  x  e.  B ) )
21alrimiv 1773 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3421 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
42, 3sylibr 216 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1442    e. wcel 1887    C_ wss 3404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-in 3411  df-ss 3418
This theorem is referenced by:  sscon  3567  ssdif  3568  unss1  3603  ssrin  3657  eq0rdv  3769  uniss  4219  intss1  4249  intmin  4254  intssuni  4257  iunss1  4290  iinss1  4291  ss2iun  4294  ssiun  4320  ssiun2  4321  iinss  4329  iinss2  4330  trintss  4513  sspwb  4649  pwssun  4740  relop  4985  dmss  5034  dmcosseq  5096  ssrnres  5275  sossfld  5283  predpo  5398  preddowncl  5407  tron  5446  tz7.7  5449  dffv2  5938  chfnrn  5993  fvn0ssdmfun  6013  fveqdmss  6017  dff3  6035  ffnfv  6049  f1imass  6165  ssorduni  6612  onint  6622  limsssuc  6677  limuni3  6679  limomss  6697  fo1stres  6817  fo2ndres  6818  fo2ndf  6903  fnse  6913  ressuppssdif  6936  suppss  6945  reldmtpos  6981  wfrlem10  7045  onfununi  7060  smoiun  7080  smorndom  7087  tz7.48-1  7160  tz7.49  7162  oaass  7262  qsss  7424  uniinqs  7443  pmss12g  7498  mapss  7514  ixpssmap2g  7551  ixpssmapg  7552  fineqv  7787  pssnn  7790  ssfii  7933  dffi2  7937  ordtypelem9  8041  ordtypelem10  8042  oismo  8055  unxpwdom2  8103  inf3lemd  8132  inf3lem1  8133  inf3lem6  8138  cantnflem3  8196  cantnf  8198  cnfcom3lem  8208  onssr1  8302  rankunb  8321  tcrank  8355  harcard  8412  carduni  8415  infxpenlem  8444  infpwfien  8493  dfac12r  8576  ackbij2lem1  8649  ackbij1lem18  8667  isfin1-3  8816  fin1a2lem11  8840  fin1a2lem13  8842  zorn2lem4  8929  zorn2lem5  8930  ttukeylem6  8944  ttukeylem7  8945  fpwwe2lem11  9065  fpwwe2lem12  9066  fpwwe2  9068  wunr1om  9144  wunom  9145  tskr1om  9192  tskr1om2  9193  tskxpss  9197  tskcard  9206  tskuni  9208  grothomex  9254  genpss  9429  distrlem1pr  9450  distrlem5pr  9452  prlem934  9458  ltexprlem2  9462  ltexprlem6  9466  ltexprlem7  9467  reclem3pr  9474  reclem4pr  9475  supaddc  10574  supadd  10575  supmul1  10576  supmullem2  10578  peano5uzi  11024  uzss  11179  ixxdisj  11650  ixxss1  11653  ixxss2  11654  ixxss12  11655  ixxub  11656  ixxlb  11657  ixxlbOLD  11658  iocssre  11714  icossre  11715  iccssre  11716  icodisj  11757  fzss1  11837  fzss2  11838  fzosplit  11951  fzouzsplit  11953  ssfzo12bi  12006  ssnn0fi  12197  fsuppmapnn0fiub  12203  suppssfz  12206  sswrd  12679  sswrdOLD  12680  rtrclreclem3  13123  isercoll  13731  summolem2a  13781  fsumcvg3  13795  fsum2dlem  13831  fsumcom2  13835  qshash  13885  prodmolem2a  13988  fprod2dlem  14034  fprodcom2  14038  bitsfzo  14409  phimullem  14727  prmreclem5  14864  1arith  14871  vdwlem2  14932  vdwlem6  14936  vdwlem8  14938  ramtlecl  14951  prmgaplem3  15023  prmgaplem4  15024  monhom  15640  epihom  15647  funcsetcres2  15988  funcestrcsetclem8  16032  funcsetcestrclem8  16047  psdmrn  16453  psssdm2  16461  gsumwspan  16630  frmdss2  16647  ssnmz  16859  conjnmz  16916  gex1  17243  sylow2alem1  17269  sylow3lem3  17281  lsmless1x  17296  lsmless2x  17297  lsmub1x  17298  lsmub2x  17299  lsmmod  17325  lsmdisj2  17332  efgrelexlemb  17400  efgcpbllemb  17405  cntzcmn  17480  gsum2d2  17606  dprdub  17658  dprdss  17662  dprddisj2  17672  ablfacrp  17699  pgpfac1lem3  17710  kerf1hrm  17971  isdrng2  17985  subrguss  18023  subrgmre  18032  lssssr  18176  lsssssubg  18181  lssmre  18189  lbspss  18305  lspdisj  18348  lbsextlem2  18382  lidl1el  18442  drngnidl  18453  lpiss  18474  unitrrg  18517  fidomndrng  18531  mplbas2  18694  zsssubrg  19026  qsssubdrg  19027  cnsubrg  19028  mulgrhm2  19070  znrrg  19136  ocvocv  19234  ocv2ss  19236  ocvin  19237  lsmcss  19255  cssmre  19256  pjfo  19278  pjcss  19279  obs2ss  19292  frlmsslsp  19354  lindfrn  19379  dmatsgrp  19524  scmatsgrp  19544  scmatsgrp1  19547  m2cpmrngiso  19782  bastg  19981  tgss  19984  tgtop  19989  tgidm  19996  en2top  20001  neisspw  20123  topssnei  20140  neiptopuni  20146  lpss3  20160  clslp  20164  tgrest  20175  ssrest  20192  restfpw  20195  restntr  20198  ordtbas2  20207  ordtbas  20208  cnss1  20292  cnss2  20293  cnsscnp  20295  cnrest2r  20303  cmpsublem  20414  cmpsub  20415  tgcmp  20416  cmpcld  20417  hauscmplem  20421  cnconn  20437  2ndcsep  20474  llyss  20494  nllyss  20495  restnlly  20497  restlly  20498  locfincmp  20541  locfincf  20546  kgenss  20558  kgenidm  20562  llycmpkgen2  20565  1stckgen  20569  kgen2ss  20570  kgencn3  20573  ptbasfi  20596  ptpjopn  20627  ptclsg  20630  txdis  20647  txkgen  20667  xkoptsub  20669  xkopjcn  20671  txcon  20704  qtoptop2  20714  qtopuni  20717  qtopkgen  20725  basqtop  20726  tgqtop  20727  qtopss  20730  qtoprest  20732  qtopomap  20733  qtopcmap  20734  kqsat  20746  kqcldsat  20748  hmphdis  20811  isfild  20873  ssfg  20887  fgss  20888  fgss2  20889  fgfil  20890  fgabs  20894  filcon  20898  fgtr  20905  trfg  20906  uzrest  20912  ufilmax  20922  ufileu  20934  filufint  20935  rnelfm  20968  fmfnfmlem2  20970  fmfnfmlem4  20972  flimss2  20987  flimss1  20988  flimclsi  20993  flimcf  20997  flimsncls  21001  fclssscls  21033  fclsss1  21037  fclsss2  21038  fclscf  21040  uffclsflim  21046  alexsublem  21059  alexsubALTlem3  21064  ptcmplem2  21068  ptcmplem3  21069  cnextf  21081  symgtgp  21116  cldsubg  21125  tsmscl  21149  haustsms2  21151  tgptsmscls  21164  tsmsxp  21169  restutop  21252  restutopopn  21253  ustuqtop4  21259  utop2nei  21265  utop3cls  21266  ucncn  21300  xblss2ps  21416  xblss2  21417  unirnblps  21434  unirnbl  21435  xrsblre  21829  xrsmopn  21830  recld2  21832  zdis  21834  icccmplem2  21841  cncfss  21931  cnheiborlem  21982  htpycn  22004  phtpyhtpy  22013  pi1blem  22070  clsocv  22221  cfilfcls  22244  iscmet3lem2  22262  iscmet2  22264  caussi  22267  equivcfil  22269  lmcau  22282  cmetss  22284  pjth  22393  hlhil  22397  ivthicc  22409  ovoliunnul  22460  ovolicopnf  22478  uniioombllem3  22543  dyadmbllem  22557  opnmbllem  22559  volsup2  22563  vitalilem2  22567  itg1addlem4  22657  itg10a  22668  itg1ge0a  22669  mbfi1fseqlem4  22676  itg2gt0  22718  limciun  22849  perfdvf  22858  dvidlem  22870  cpnord  22889  dvaddf  22896  dvmulf  22897  dvcof  22902  dvcj  22904  dvrec  22909  dvcnv  22929  dvlip2  22947  dvivth  22962  dvne0  22963  dvcnvre  22971  ftc1cn  22995  ply1lpir  23136  plyco0  23146  plyexmo  23266  ulmdv  23358  pserdv  23384  abelth  23396  efif1o  23495  logno1  23581  efopnlem2  23602  loglesqrt  23698  lgamcvg2  23980  ppisval  24030  ppisval2  24031  ppinprm  24079  chtnprm  24081  fsumvma  24141  dchrfi  24183  chtppilimlem2  24312  chebbnd2  24315  vmadivsumb  24321  rplogsumlem2  24323  dchrisumlem2  24328  vmalogdivsum2  24376  vmalogdivsum  24377  2vmadivsumlem  24378  selbergb  24387  selberg2b  24390  selberg3lem1  24395  selberg3lem2  24396  selberg3  24397  selberg4lem1  24398  selberg4  24399  pntrlog2bndlem2  24416  pntrlog2bndlem4  24418  sizeusglecusglem1  25212  clwwlkssclwwlkn  25520  ococss  26946  shsub1  26977  shless  27012  shmodsi  27042  pjhth  27046  spansnss  27224  spanpr  27233  spansnm0i  27303  pjjsi  27353  sumdmdii  28068  sumdmdlem  28071  sumdmdlem2  28072  cdj3lem1  28087  abrexss  28146  rnmpt2ss  28276  unifi3  28293  ssnnssfz  28367  reff  28666  crefss  28676  cmpcref  28677  tpr2rico  28718  esumrnmpt2  28889  esumpcvgval  28899  ldsysgenld  28982  sigapildsys  28984  ldgenpisys  28988  cldssbrsiga  29009  measdivcstOLD  29046  mbfmcnt  29090  dya2iocuni  29105  oddpwdc  29187  eulerpartlemgs2  29213  bnj1033  29778  bnj1398  29843  sconpi1  29962  cvmscld  29996  cvmsss2  29997  cvmliftlem15  30021  dfon2lem6  30434  nofulllem5  30595  fnessref  31013  fgmin  31026  tailfb  31033  dissneqlem  31742  icoreresf  31755  finxpreclem6  31788  poimirlem11  31951  poimirlem12  31952  opnmbllem0  31976  ftc1cnnc  32016  sstotbnd3  32108  prdstotbnd  32126  cntotbnd  32128  ismtyhmeo  32137  1idl  32259  lshpdisj  32553  lssats  32578  lkrlsp  32668  lkrin  32730  glbconxN  32943  paddss1  33382  paddss2  33383  paddasslem16  33400  paddidm  33406  pmodlem2  33412  pmapjoin  33417  pmapjat1  33418  pclfinN  33465  pclfinclN  33515  cdleme50rnlem  34111  diasslssN  34627  dia2dimlem12  34643  dihsslss  34844  baerlem3lem2  35278  baerlem5alem2  35279  baerlem5blem2  35280  hdmaprnN  35435  hgmaprnN  35472  eldiophss  35617  rencldnfilem  35663  pellexlem5  35677  pell14qrss1234  35702  pell1qrss14  35714  pellfundre  35729  pellfundge  35730  pellfundlb  35732  pellfundglb  35733  harinf  35889  kercvrlsm  35941  pwssplit4  35947  hbtlem5  35987  proot1hash  36077  intabssd  36216  ss2iundf  36251  ov2ssiunov2  36292  radcnvrat  36663  nznngen  36665  trsspwALT3  37208  sspwimpALT2  37325  refsumcn  37351  icoiccdif  37625  lptioo2  37711  lptioo1  37712  icccncfext  37765  stoweidlem27  37887  stoweidlem46  37907  stoweidlem57  37918  fourierdlem40  38010  fourierdlem78  38048  ffnafv  38673  iccpartrn  38744  elpwdifsn  38990  uhgredgss  39222  usgruspgrb  39268  uhgrissubgr  39347  uhgrspansubgrlem  39362  uhgrspan1  39375  nbgrssvtx  39428  nbgrssovtx  39432  cusgredg  39492  usgredgsscusgredg  39520  rnghmsscmap2  40028  rnghmsscmap  40029  funcrngcsetc  40053  funcrngcsetcALT  40054  rhmsscmap2  40074  rhmsscmap  40075  rhmsscrnghm  40081  rngcresringcat  40085  funcringcsetc  40090  funcringcsetcALTV2lem8  40098  funcringcsetclem8ALTV  40121  rhmsubcALTVlem4  40163  ssnn0ssfz  40183  lincolss  40280  lcoss  40282  lcosslsp  40284
  Copyright terms: Public domain W3C validator