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

Theorem ssrdv 3424
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 1781 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3407 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
42, 3sylibr 217 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1450    e. wcel 1904    C_ wss 3390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404
This theorem is referenced by:  sscon  3556  ssdif  3557  unss1  3594  ssrin  3648  eq0rdv  3773  uniss  4211  intss1  4241  intmin  4246  intssuni  4248  iunss1  4281  iinss1  4282  ss2iun  4285  ssiun  4311  ssiun2  4312  iinss  4320  iinss2  4321  trintss  4506  sspwb  4649  pwssun  4745  relop  4990  dmss  5039  dmcosseq  5102  ssrnres  5281  sossfld  5289  predpo  5405  preddowncl  5414  tron  5453  tz7.7  5456  dffv2  5953  chfnrn  6008  fvn0ssdmfun  6028  fveqdmss  6032  dff3  6050  ffnfv  6064  f1imass  6183  ssorduni  6631  onint  6641  limsssuc  6696  limuni3  6698  limomss  6716  fo1stres  6836  fo2ndres  6837  fo2ndf  6922  fnse  6932  ressuppssdif  6955  suppss  6964  reldmtpos  6999  wfrlem10  7063  onfununi  7078  smoiun  7098  smorndom  7105  tz7.48-1  7178  tz7.49  7180  oaass  7280  qsss  7442  uniinqs  7461  pmss12g  7516  mapss  7532  ixpssmap2g  7569  ixpssmapg  7570  fineqv  7805  pssnn  7808  ssfii  7951  dffi2  7955  ordtypelem9  8059  ordtypelem10  8060  oismo  8073  unxpwdom2  8121  inf3lemd  8150  inf3lem1  8151  inf3lem6  8156  cantnflem3  8214  cantnf  8216  cnfcom3lem  8226  onssr1  8320  rankunb  8339  tcrank  8373  harcard  8430  carduni  8433  infxpenlem  8462  infpwfien  8511  dfac12r  8594  ackbij2lem1  8667  ackbij1lem18  8685  isfin1-3  8834  fin1a2lem11  8858  fin1a2lem13  8860  zorn2lem4  8947  zorn2lem5  8948  ttukeylem6  8962  ttukeylem7  8963  fpwwe2lem11  9083  fpwwe2lem12  9084  fpwwe2  9086  wunr1om  9162  wunom  9163  tskr1om  9210  tskr1om2  9211  tskxpss  9215  tskcard  9224  tskuni  9226  grothomex  9272  genpss  9447  distrlem1pr  9468  distrlem5pr  9470  prlem934  9476  ltexprlem2  9480  ltexprlem6  9484  ltexprlem7  9485  reclem3pr  9492  reclem4pr  9493  supaddc  10596  supadd  10597  supmul1  10598  supmullem2  10600  peano5uzi  11047  uzss  11203  ixxdisj  11675  ixxss1  11678  ixxss2  11679  ixxss12  11680  ixxub  11681  ixxlb  11682  ixxlbOLD  11683  iocssre  11739  icossre  11740  iccssre  11741  icodisj  11783  fzss1  11863  fzss2  11864  fzosplit  11978  fzouzsplit  11980  ssfzo12bi  12035  ssnn0fi  12235  fsuppmapnn0fiub  12241  suppssfz  12244  sswrd  12726  sswrdOLD  12727  rtrclreclem3  13200  isercoll  13808  summolem2a  13858  fsumcvg3  13872  fsum2dlem  13908  fsumcom2  13912  qshash  13962  prodmolem2a  14065  fprod2dlem  14111  fprodcom2  14115  bitsfzo  14488  phimullem  14806  prmreclem5  14943  1arith  14950  vdwlem2  15011  vdwlem6  15015  vdwlem8  15017  ramtlecl  15030  prmgaplem3  15102  prmgaplem4  15103  monhom  15718  epihom  15725  funcsetcres2  16066  funcestrcsetclem8  16110  funcsetcestrclem8  16125  psdmrn  16531  psssdm2  16539  gsumwspan  16708  frmdss2  16725  ssnmz  16937  conjnmz  16994  gex1  17321  sylow2alem1  17347  sylow3lem3  17359  lsmless1x  17374  lsmless2x  17375  lsmub1x  17376  lsmub2x  17377  lsmmod  17403  lsmdisj2  17410  efgrelexlemb  17478  efgcpbllemb  17483  cntzcmn  17558  gsum2d2  17684  dprdub  17736  dprdss  17740  dprddisj2  17750  ablfacrp  17777  pgpfac1lem3  17788  kerf1hrm  18049  isdrng2  18063  subrguss  18101  subrgmre  18110  lssssr  18254  lsssssubg  18259  lssmre  18267  lbspss  18383  lspdisj  18426  lbsextlem2  18460  lidl1el  18519  drngnidl  18530  lpiss  18551  unitrrg  18594  fidomndrng  18608  mplbas2  18771  zsssubrg  19103  qsssubdrg  19104  cnsubrg  19105  mulgrhm2  19147  znrrg  19213  ocvocv  19311  ocv2ss  19313  ocvin  19314  lsmcss  19332  cssmre  19333  pjfo  19355  pjcss  19356  obs2ss  19369  frlmsslsp  19431  lindfrn  19456  dmatsgrp  19601  scmatsgrp  19621  scmatsgrp1  19624  m2cpmrngiso  19859  bastg  20058  tgss  20061  tgtop  20066  tgidm  20073  en2top  20078  neisspw  20200  topssnei  20217  neiptopuni  20223  lpss3  20237  clslp  20241  tgrest  20252  ssrest  20269  restfpw  20272  restntr  20275  ordtbas2  20284  ordtbas  20285  cnss1  20369  cnss2  20370  cnsscnp  20372  cnrest2r  20380  cmpsublem  20491  cmpsub  20492  tgcmp  20493  cmpcld  20494  hauscmplem  20498  cnconn  20514  2ndcsep  20551  llyss  20571  nllyss  20572  restnlly  20574  restlly  20575  locfincmp  20618  locfincf  20623  kgenss  20635  kgenidm  20639  llycmpkgen2  20642  1stckgen  20646  kgen2ss  20647  kgencn3  20650  ptbasfi  20673  ptpjopn  20704  ptclsg  20707  txdis  20724  txkgen  20744  xkoptsub  20746  xkopjcn  20748  txcon  20781  qtoptop2  20791  qtopuni  20794  qtopkgen  20802  basqtop  20803  tgqtop  20804  qtopss  20807  qtoprest  20809  qtopomap  20810  qtopcmap  20811  kqsat  20823  kqcldsat  20825  hmphdis  20888  isfild  20951  ssfg  20965  fgss  20966  fgss2  20967  fgfil  20968  fgabs  20972  filcon  20976  fgtr  20983  trfg  20984  uzrest  20990  ufilmax  21000  ufileu  21012  filufint  21013  rnelfm  21046  fmfnfmlem2  21048  fmfnfmlem4  21050  flimss2  21065  flimss1  21066  flimclsi  21071  flimcf  21075  flimsncls  21079  fclssscls  21111  fclsss1  21115  fclsss2  21116  fclscf  21118  uffclsflim  21124  alexsublem  21137  alexsubALTlem3  21142  ptcmplem2  21146  ptcmplem3  21147  cnextf  21159  symgtgp  21194  cldsubg  21203  tsmscl  21227  haustsms2  21229  tgptsmscls  21242  tsmsxp  21247  restutop  21330  restutopopn  21331  ustuqtop4  21337  utop2nei  21343  utop3cls  21344  ucncn  21378  xblss2ps  21494  xblss2  21495  unirnblps  21512  unirnbl  21513  xrsblre  21907  xrsmopn  21908  recld2  21910  zdis  21912  icccmplem2  21919  cncfss  22009  cnheiborlem  22060  htpycn  22082  phtpyhtpy  22091  pi1blem  22148  clsocv  22299  cfilfcls  22322  iscmet3lem2  22340  iscmet2  22342  caussi  22345  equivcfil  22347  lmcau  22360  cmetss  22362  pjth  22471  hlhil  22475  ivthicc  22487  ovoliunnul  22538  ovolicopnf  22556  uniioombllem3  22622  dyadmbllem  22636  opnmbllem  22638  volsup2  22642  vitalilem2  22646  itg1addlem4  22736  itg10a  22747  itg1ge0a  22748  mbfi1fseqlem4  22755  itg2gt0  22797  limciun  22928  perfdvf  22937  dvidlem  22949  cpnord  22968  dvaddf  22975  dvmulf  22976  dvcof  22981  dvcj  22983  dvrec  22988  dvcnv  23008  dvlip2  23026  dvivth  23041  dvne0  23042  dvcnvre  23050  ftc1cn  23074  ply1lpir  23215  plyco0  23225  plyexmo  23345  ulmdv  23437  pserdv  23463  abelth  23475  efif1o  23574  logno1  23660  efopnlem2  23681  loglesqrt  23777  lgamcvg2  24059  ppisval  24109  ppisval2  24110  ppinprm  24158  chtnprm  24160  fsumvma  24220  dchrfi  24262  chtppilimlem2  24391  chebbnd2  24394  vmadivsumb  24400  rplogsumlem2  24402  dchrisumlem2  24407  vmalogdivsum2  24455  vmalogdivsum  24456  2vmadivsumlem  24457  selbergb  24466  selberg2b  24469  selberg3lem1  24474  selberg3lem2  24475  selberg3  24476  selberg4lem1  24477  selberg4  24478  pntrlog2bndlem2  24495  pntrlog2bndlem4  24497  sizeusglecusglem1  25291  clwwlkssclwwlkn  25599  ococss  27027  shsub1  27058  shless  27093  shmodsi  27123  pjhth  27127  spansnss  27305  spanpr  27314  spansnm0i  27384  pjjsi  27434  sumdmdii  28149  sumdmdlem  28152  sumdmdlem2  28153  cdj3lem1  28168  abrexss  28225  rnmpt2ss  28351  unifi3  28368  ssnnssfz  28442  reff  28740  crefss  28750  cmpcref  28751  tpr2rico  28792  esumrnmpt2  28963  esumpcvgval  28973  ldsysgenld  29056  sigapildsys  29058  ldgenpisys  29062  cldssbrsiga  29083  measdivcstOLD  29120  mbfmcnt  29163  dya2iocuni  29178  oddpwdc  29260  eulerpartlemgs2  29286  bnj1033  29850  bnj1398  29915  sconpi1  30034  cvmscld  30068  cvmsss2  30069  cvmliftlem15  30093  dfon2lem6  30505  nofulllem5  30666  fnessref  31084  fgmin  31097  tailfb  31104  dissneqlem  31812  icoreresf  31825  finxpreclem6  31858  poimirlem11  32015  poimirlem12  32016  opnmbllem0  32040  ftc1cnnc  32080  sstotbnd3  32172  prdstotbnd  32190  cntotbnd  32192  ismtyhmeo  32201  1idl  32323  lshpdisj  32624  lssats  32649  lkrlsp  32739  lkrin  32801  glbconxN  33014  paddss1  33453  paddss2  33454  paddasslem16  33471  paddidm  33477  pmodlem2  33483  pmapjoin  33488  pmapjat1  33489  pclfinN  33536  pclfinclN  33586  cdleme50rnlem  34182  diasslssN  34698  dia2dimlem12  34714  dihsslss  34915  baerlem3lem2  35349  baerlem5alem2  35350  baerlem5blem2  35351  hdmaprnN  35506  hgmaprnN  35543  eldiophss  35688  rencldnfilem  35734  pellexlem5  35748  pell14qrss1234  35773  pell1qrss14  35785  pellfundre  35800  pellfundge  35801  pellfundlb  35803  pellfundglb  35804  harinf  35960  kercvrlsm  36012  pwssplit4  36018  hbtlem5  36058  proot1hash  36148  intabssd  36287  ss2iundf  36322  ov2ssiunov2  36363  radcnvrat  36733  nznngen  36735  trsspwALT3  37271  sspwimpALT2  37388  refsumcn  37414  icoiccdif  37721  lptioo2  37808  lptioo1  37809  icccncfext  37862  stoweidlem27  37999  stoweidlem46  38019  stoweidlem57  38030  fourierdlem40  38122  fourierdlem78  38160  ffnafv  38818  iccpartrn  38889  elpwdifsn  39137  uhgredgss  39383  usgruspgrb  39429  uhgrissubgr  39511  uhgrspansubgrlem  39526  uhgrspan1  39539  nbgrssvtx  39592  nbgrssovtx  39596  cusgredg  39656  usgredgsscusgredg  39685  rnghmsscmap2  40483  rnghmsscmap  40484  funcrngcsetc  40508  funcrngcsetcALT  40509  rhmsscmap2  40529  rhmsscmap  40530  rhmsscrnghm  40536  rngcresringcat  40540  funcringcsetc  40545  funcringcsetcALTV2lem8  40553  funcringcsetclem8ALTV  40576  rhmsubcALTVlem4  40618  ssnn0ssfz  40638  lincolss  40735  lcoss  40737  lcosslsp  40739
  Copyright terms: Public domain W3C validator