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

Theorem ssrdv 3290
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 1638 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3273 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
42, 3sylibr 204 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1546    e. wcel 1717    C_ wss 3256
This theorem is referenced by:  sscon  3417  ssdif  3418  unss1  3452  ssrin  3502  eq0rdv  3598  uniss  3971  intss1  4000  intmin  4005  intssuni  4007  iunss1  4039  iinss1  4040  ss2iun  4043  ssiun  4067  ssiun2  4068  iinss  4076  iinss2  4077  trintss  4252  sspwb  4347  pwssun  4423  tron  4538  tz7.7  4541  ssorduni  4699  onint  4708  limsssuc  4763  limuni3  4765  limomss  4783  xpsspw  4919  relop  4956  dmss  5002  dmcosseq  5070  ssrnres  5242  sossfld  5250  dffv2  5728  chfnrn  5773  suppss  5795  dff3  5814  ffnfv  5826  f1imass  5942  fo1stres  6302  fo2ndres  6303  fnse  6392  reldmtpos  6416  onfununi  6532  smoiun  6552  smorndom  6559  tz7.48-1  6629  tz7.49  6631  oaass  6733  qsss  6894  uniinqs  6913  pmss12g  6969  mapss  6985  ixpssmap2g  7020  ixpssmapg  7021  fineqv  7253  pssnn  7256  ssfii  7352  dffi2  7356  ordtypelem9  7421  ordtypelem10  7422  oismo  7435  unxpwdom2  7482  inf3lemd  7508  inf3lem1  7509  inf3lem6  7514  cantnflem3  7573  cantnf  7575  cnfcom3lem  7586  onssr1  7683  rankunb  7702  tcrank  7734  harcard  7791  carduni  7794  infxpenlem  7821  infpwfien  7869  dfac12r  7952  ackbij2lem1  8025  ackbij1lem18  8043  isfin1-3  8192  fin1a2lem11  8216  fin1a2lem13  8218  zorn2lem4  8305  zorn2lem5  8306  ttukeylem6  8320  ttukeylem7  8321  fpwwe2lem11  8441  fpwwe2lem12  8442  fpwwe2  8444  wunr1om  8520  wunom  8521  tskr1om  8568  tskr1om2  8569  tskxpss  8573  tskcard  8582  tskuni  8584  grothomex  8630  genpss  8807  distrlem1pr  8828  distrlem5pr  8830  prlem934  8836  ltexprlem2  8840  ltexprlem6  8844  ltexprlem7  8845  reclem3pr  8852  reclem4pr  8853  supmul1  9898  supmullem2  9900  peano5uzi  10283  uzss  10431  ixxdisj  10856  ixxss1  10859  ixxss2  10860  ixxss12  10861  ixxub  10862  ixxlb  10863  iocssre  10915  icossre  10916  iccssre  10917  icodisj  10947  fzss1  11016  fzss2  11017  fzosplit  11089  fzouzsplit  11091  sswrd  11657  isercoll  12381  summolem2a  12429  fsumcvg3  12443  fsum2dlem  12474  fsumcom2  12478  qshash  12526  bitsfzo  12867  phimullem  13088  prmreclem5  13208  1arith  13215  vdwlem2  13270  vdwlem6  13274  vdwlem8  13276  ramtlecl  13288  monhom  13881  epihom  13888  funcsetcres2  14168  psdmrn  14559  psssdm2  14567  gsumwspan  14711  frmdss2  14728  ssnmz  14902  conjnmz  14959  gex1  15145  sylow2alem1  15171  sylow3lem3  15183  lsmless1x  15198  lsmless2x  15199  lsmub1x  15200  lsmub2x  15201  lsmmod  15227  lsmdisj2  15234  efgrelexlemb  15302  efgcpbllemb  15307  cntzcmn  15379  gsum2d2  15468  dprdub  15503  dprdss  15507  dprddisj2  15517  ablfacrp  15544  pgpfac1lem3  15555  isdrng2  15765  subrguss  15803  subrgmre  15812  lssssr  15949  lsssssubg  15954  lssmre  15962  lbspss  16074  lspdisj  16117  lbsextlem2  16151  lidl1el  16209  drngnidl  16220  lpiss  16241  unitrrg  16273  fidomndrng  16287  mplbas2  16451  zsssubrg  16673  qsssubdrg  16674  cnsubrg  16675  mulgrhm2  16704  znrrg  16762  ocvocv  16814  ocv2ss  16816  ocvin  16817  lsmcss  16835  cssmre  16836  pjfo  16858  pjcss  16859  obs2ss  16872  bastg  16947  tgss  16949  tgtop  16954  tgidm  16961  en2top  16966  neisspw  17087  topssnei  17104  neiptopuni  17110  lpss3  17124  clslp  17127  tgrest  17138  ssrest  17155  restfpw  17158  restntr  17161  ordtbas2  17170  ordtbas  17171  cnss1  17255  cnss2  17256  cnsscnp  17258  cnrest2r  17266  cmpsublem  17377  cmpsub  17378  tgcmp  17379  cmpcld  17380  hauscmplem  17384  cnconn  17399  2ndcsep  17436  llyss  17456  nllyss  17457  restnlly  17459  restlly  17460  kgenss  17489  kgenidm  17493  llycmpkgen2  17496  1stckgen  17500  kgen2ss  17501  kgencn3  17504  ptbasfi  17527  ptpjopn  17558  ptclsg  17561  txdis  17578  txkgen  17598  xkoptsub  17600  xkopjcn  17602  txcon  17635  qtoptop2  17645  qtopuni  17648  qtopkgen  17656  basqtop  17657  tgqtop  17658  qtopss  17661  qtoprest  17663  qtopomap  17664  qtopcmap  17665  kqsat  17677  kqcldsat  17679  hmphdis  17742  isfild  17804  ssfg  17818  fgss  17819  fgss2  17820  fgfil  17821  fgabs  17825  filcon  17829  fgtr  17836  trfg  17837  uzrest  17843  ufilmax  17853  ufileu  17865  filufint  17866  rnelfm  17899  fmfnfmlem2  17901  fmfnfmlem4  17903  flimss2  17918  flimss1  17919  flimclsi  17924  flimcf  17928  flimsncls  17932  fclssscls  17964  fclsss1  17968  fclsss2  17969  fclscf  17971  uffclsflim  17977  alexsublem  17989  alexsubALTlem3  17994  ptcmplem2  17998  ptcmplem3  17999  cnextf  18011  symgtgp  18045  cldsubg  18054  tsmscl  18078  haustsms2  18080  tgptsmscls  18093  tsmsxp  18098  restutop  18181  restutopopn  18182  ustuqtop4  18188  utop2nei  18194  utop3cls  18195  ucncn  18229  xblss2  18325  unirnbl  18336  xrsblre  18706  xrsmopn  18707  recld2  18709  zdis  18711  icccmplem2  18718  cncfss  18793  cnheiborlem  18843  htpycn  18862  phtpyhtpy  18871  pi1blem  18928  clsocv  19068  cfilfcls  19091  iscmet3lem2  19109  iscmet2  19111  caussi  19114  equivcfil  19116  lmcau  19129  cmetss  19131  pjth  19200  hlhil  19204  ivthicc  19215  ovoliunnul  19263  ovolicopnf  19280  uniioombllem3  19337  dyadmbllem  19351  opnmbllem  19353  volsup2  19357  vitalilem2  19361  itg1addlem4  19451  itg10a  19462  itg1ge0a  19463  mbfi1fseqlem4  19470  itg2gt0  19512  limciun  19641  perfdvf  19650  dvidlem  19662  cpnord  19681  dvaddf  19688  dvmulf  19689  dvcof  19694  dvcj  19696  dvrec  19701  dvcnv  19721  dvlip2  19739  dvivth  19754  dvne0  19755  dvcnvre  19763  ftc1cn  19787  ply1lpir  19961  plyco0  19971  plyexmo  20090  ulmdv  20179  pserdv  20205  abelth  20217  efif1o  20308  logno1  20387  efopnlem2  20408  loglesqr  20502  ppisval  20746  ppisval2  20747  ppinprm  20795  chtnprm  20797  fsumvma  20857  dchrfi  20899  chtppilimlem2  21028  chebbnd2  21031  vmadivsumb  21037  rplogsumlem2  21039  dchrisumlem2  21044  vmalogdivsum2  21092  vmalogdivsum  21093  2vmadivsumlem  21094  selbergb  21103  selberg2b  21106  selberg3lem1  21111  selberg3lem2  21112  selberg3  21113  selberg4lem1  21114  selberg4  21115  pntrlog2bndlem2  21132  pntrlog2bndlem4  21134  sizeusglecusglem1  21352  ococss  22636  shsub1  22667  shless  22702  shmodsi  22732  pjhth  22736  spansnss  22914  spanpr  22923  spansnm0i  22993  pjjsi  23043  sumdmdii  23759  sumdmdlem  23762  sumdmdlem2  23763  cdj3lem1  23778  abrexss  23830  rnmpt2ss  23920  ssnnssfz  23977  kerf1hrm  24071  tpr2rico  24107  esumpcvgval  24257  cldssbrsiga  24330  measdivcstOLD  24365  mbfmcnt  24405  dya2iocuni  24420  lgamcvg2  24611  sconpi1  24698  cvmscld  24732  cvmsss2  24733  cvmliftlem15  24757  rtrclreclem.trans  24918  prodmolem2a  25032  dfon2lem6  25161  predpo  25201  preddowncl  25213  wfrlem10  25282  nofulllem5  25377  supaddc  25940  supadd  25941  ftc1cnnc  25972  fnessref  26057  locfincmp  26068  locfincf  26070  fgmin  26083  tailfb  26090  sstotbnd3  26169  prdstotbnd  26187  cntotbnd  26189  ismtyhmeo  26198  1idl  26320  eldiophss  26517  rencldnfilem  26565  pellexlem5  26580  pell14qrss1234  26603  pell1qrss14  26615  pellfundre  26628  pellfundge  26629  pellfundlb  26631  pellfundglb  26632  harinf  26789  kercvrlsm  26843  pwssplit4  26853  frlmsslsp  26910  lindfrn  26953  hbtlem5  26994  proot1hash  27181  refsumcn  27362  stoweidlem27  27437  stoweidlem46  27456  stoweidlem57  27467  ffnafv  27697  trsspwALT3  28267  sspwimpALT2  28375  bnj1033  28669  bnj1398  28734  lshpdisj  29153  lssats  29178  lkrlsp  29268  lkrin  29330  glbconxN  29543  paddss1  29982  paddss2  29983  paddasslem16  30000  paddidm  30006  pmodlem2  30012  pmapjoin  30017  pmapjat1  30018  pclfinN  30065  pclfinclN  30115  cdleme50rnlem  30709  diasslssN  31225  dia2dimlem12  31241  dihsslss  31442  baerlem3lem2  31876  baerlem5alem2  31877  baerlem5blem2  31878  hdmaprnN  32033  hgmaprnN  32070
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-in 3263  df-ss 3270
  Copyright terms: Public domain W3C validator