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

Theorem ssrdv 3297
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 3280 . 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 3263
This theorem is referenced by:  sscon  3424  ssdif  3425  unss1  3459  ssrin  3509  eq0rdv  3605  uniss  3978  intss1  4007  intmin  4012  intssuni  4014  iunss1  4046  iinss1  4047  ss2iun  4050  ssiun  4074  ssiun2  4075  iinss  4083  iinss2  4084  trintss  4259  sspwb  4354  pwssun  4430  tron  4545  tz7.7  4548  ssorduni  4706  onint  4715  limsssuc  4770  limuni3  4772  limomss  4790  xpsspw  4926  relop  4963  dmss  5009  dmcosseq  5077  ssrnres  5249  sossfld  5257  dffv2  5735  chfnrn  5780  suppss  5802  dff3  5821  ffnfv  5833  f1imass  5949  fo1stres  6309  fo2ndres  6310  fnse  6399  reldmtpos  6423  onfununi  6539  smoiun  6559  smorndom  6566  tz7.48-1  6636  tz7.49  6638  oaass  6740  qsss  6901  uniinqs  6920  pmss12g  6976  mapss  6992  ixpssmap2g  7027  ixpssmapg  7028  fineqv  7260  pssnn  7263  ssfii  7359  dffi2  7363  ordtypelem9  7428  ordtypelem10  7429  oismo  7442  unxpwdom2  7489  inf3lemd  7515  inf3lem1  7516  inf3lem6  7521  cantnflem3  7580  cantnf  7582  cnfcom3lem  7593  onssr1  7690  rankunb  7709  tcrank  7741  harcard  7798  carduni  7801  infxpenlem  7828  infpwfien  7876  dfac12r  7959  ackbij2lem1  8032  ackbij1lem18  8050  isfin1-3  8199  fin1a2lem11  8223  fin1a2lem13  8225  zorn2lem4  8312  zorn2lem5  8313  ttukeylem6  8327  ttukeylem7  8328  fpwwe2lem11  8448  fpwwe2lem12  8449  fpwwe2  8451  wunr1om  8527  wunom  8528  tskr1om  8575  tskr1om2  8576  tskxpss  8580  tskcard  8589  tskuni  8591  grothomex  8637  genpss  8814  distrlem1pr  8835  distrlem5pr  8837  prlem934  8843  ltexprlem2  8847  ltexprlem6  8851  ltexprlem7  8852  reclem3pr  8859  reclem4pr  8860  supmul1  9905  supmullem2  9907  peano5uzi  10290  uzss  10438  ixxdisj  10863  ixxss1  10866  ixxss2  10867  ixxss12  10868  ixxub  10869  ixxlb  10870  iocssre  10922  icossre  10923  iccssre  10924  icodisj  10954  fzss1  11023  fzss2  11024  fzosplit  11096  fzouzsplit  11098  sswrd  11664  isercoll  12388  summolem2a  12436  fsumcvg3  12450  fsum2dlem  12481  fsumcom2  12485  qshash  12533  bitsfzo  12874  phimullem  13095  prmreclem5  13215  1arith  13222  vdwlem2  13277  vdwlem6  13281  vdwlem8  13283  ramtlecl  13295  monhom  13888  epihom  13895  funcsetcres2  14175  psdmrn  14566  psssdm2  14574  gsumwspan  14718  frmdss2  14735  ssnmz  14909  conjnmz  14966  gex1  15152  sylow2alem1  15178  sylow3lem3  15190  lsmless1x  15205  lsmless2x  15206  lsmub1x  15207  lsmub2x  15208  lsmmod  15234  lsmdisj2  15241  efgrelexlemb  15309  efgcpbllemb  15314  cntzcmn  15386  gsum2d2  15475  dprdub  15510  dprdss  15514  dprddisj2  15524  ablfacrp  15551  pgpfac1lem3  15562  isdrng2  15772  subrguss  15810  subrgmre  15819  lssssr  15956  lsssssubg  15961  lssmre  15969  lbspss  16081  lspdisj  16124  lbsextlem2  16158  lidl1el  16216  drngnidl  16227  lpiss  16248  unitrrg  16280  fidomndrng  16294  mplbas2  16458  zsssubrg  16680  qsssubdrg  16681  cnsubrg  16682  mulgrhm2  16711  znrrg  16769  ocvocv  16821  ocv2ss  16823  ocvin  16824  lsmcss  16842  cssmre  16843  pjfo  16865  pjcss  16866  obs2ss  16879  bastg  16954  tgss  16956  tgtop  16961  tgidm  16968  en2top  16973  neisspw  17094  topssnei  17111  neiptopuni  17117  lpss3  17131  clslp  17134  tgrest  17145  ssrest  17162  restfpw  17165  restntr  17168  ordtbas2  17177  ordtbas  17178  cnss1  17262  cnss2  17263  cnsscnp  17265  cnrest2r  17273  cmpsublem  17384  cmpsub  17385  tgcmp  17386  cmpcld  17387  hauscmplem  17391  cnconn  17406  2ndcsep  17443  llyss  17463  nllyss  17464  restnlly  17466  restlly  17467  kgenss  17496  kgenidm  17500  llycmpkgen2  17503  1stckgen  17507  kgen2ss  17508  kgencn3  17511  ptbasfi  17534  ptpjopn  17565  ptclsg  17568  txdis  17585  txkgen  17605  xkoptsub  17607  xkopjcn  17609  txcon  17642  qtoptop2  17652  qtopuni  17655  qtopkgen  17663  basqtop  17664  tgqtop  17665  qtopss  17668  qtoprest  17670  qtopomap  17671  qtopcmap  17672  kqsat  17684  kqcldsat  17686  hmphdis  17749  isfild  17811  ssfg  17825  fgss  17826  fgss2  17827  fgfil  17828  fgabs  17832  filcon  17836  fgtr  17843  trfg  17844  uzrest  17850  ufilmax  17860  ufileu  17872  filufint  17873  rnelfm  17906  fmfnfmlem2  17908  fmfnfmlem4  17910  flimss2  17925  flimss1  17926  flimclsi  17931  flimcf  17935  flimsncls  17939  fclssscls  17971  fclsss1  17975  fclsss2  17976  fclscf  17978  uffclsflim  17984  alexsublem  17996  alexsubALTlem3  18001  ptcmplem2  18005  ptcmplem3  18006  cnextf  18018  symgtgp  18052  cldsubg  18061  tsmscl  18085  haustsms2  18087  tgptsmscls  18100  tsmsxp  18105  restutop  18188  restutopopn  18189  ustuqtop4  18195  utop2nei  18201  utop3cls  18202  ucncn  18236  xblss2  18332  unirnbl  18343  xrsblre  18713  xrsmopn  18714  recld2  18716  zdis  18718  icccmplem2  18725  cncfss  18800  cnheiborlem  18850  htpycn  18869  phtpyhtpy  18878  pi1blem  18935  clsocv  19075  cfilfcls  19098  iscmet3lem2  19116  iscmet2  19118  caussi  19121  equivcfil  19123  lmcau  19136  cmetss  19138  pjth  19207  hlhil  19211  ivthicc  19222  ovoliunnul  19270  ovolicopnf  19287  uniioombllem3  19344  dyadmbllem  19358  opnmbllem  19360  volsup2  19364  vitalilem2  19368  itg1addlem4  19458  itg10a  19469  itg1ge0a  19470  mbfi1fseqlem4  19477  itg2gt0  19519  limciun  19648  perfdvf  19657  dvidlem  19669  cpnord  19688  dvaddf  19695  dvmulf  19696  dvcof  19701  dvcj  19703  dvrec  19708  dvcnv  19728  dvlip2  19746  dvivth  19761  dvne0  19762  dvcnvre  19770  ftc1cn  19794  ply1lpir  19968  plyco0  19978  plyexmo  20097  ulmdv  20186  pserdv  20212  abelth  20224  efif1o  20315  logno1  20394  efopnlem2  20415  loglesqr  20509  ppisval  20753  ppisval2  20754  ppinprm  20802  chtnprm  20804  fsumvma  20864  dchrfi  20906  chtppilimlem2  21035  chebbnd2  21038  vmadivsumb  21044  rplogsumlem2  21046  dchrisumlem2  21051  vmalogdivsum2  21099  vmalogdivsum  21100  2vmadivsumlem  21101  selbergb  21110  selberg2b  21113  selberg3lem1  21118  selberg3lem2  21119  selberg3  21120  selberg4lem1  21121  selberg4  21122  pntrlog2bndlem2  21139  pntrlog2bndlem4  21141  sizeusglecusglem1  21359  ococss  22643  shsub1  22674  shless  22709  shmodsi  22739  pjhth  22743  spansnss  22921  spanpr  22930  spansnm0i  23000  pjjsi  23050  sumdmdii  23766  sumdmdlem  23769  sumdmdlem2  23770  cdj3lem1  23785  abrexss  23837  rnmpt2ss  23927  ssnnssfz  23984  kerf1hrm  24078  tpr2rico  24114  esumpcvgval  24264  cldssbrsiga  24337  measdivcstOLD  24372  mbfmcnt  24412  dya2iocuni  24427  lgamcvg2  24618  sconpi1  24705  cvmscld  24739  cvmsss2  24740  cvmliftlem15  24764  rtrclreclem.trans  24925  prodmolem2a  25039  dfon2lem6  25168  predpo  25208  preddowncl  25220  wfrlem10  25289  nofulllem5  25384  supaddc  25947  supadd  25948  ftc1cnnc  25979  fnessref  26064  locfincmp  26075  locfincf  26077  fgmin  26090  tailfb  26097  sstotbnd3  26176  prdstotbnd  26194  cntotbnd  26196  ismtyhmeo  26205  1idl  26327  eldiophss  26524  rencldnfilem  26572  pellexlem5  26587  pell14qrss1234  26610  pell1qrss14  26622  pellfundre  26635  pellfundge  26636  pellfundlb  26638  pellfundglb  26639  harinf  26796  kercvrlsm  26850  pwssplit4  26860  frlmsslsp  26917  lindfrn  26960  hbtlem5  27001  proot1hash  27188  refsumcn  27369  stoweidlem27  27444  stoweidlem46  27463  stoweidlem57  27474  ffnafv  27704  trsspwALT3  28274  sspwimpALT2  28382  bnj1033  28676  bnj1398  28741  lshpdisj  29102  lssats  29127  lkrlsp  29217  lkrin  29279  glbconxN  29492  paddss1  29931  paddss2  29932  paddasslem16  29949  paddidm  29955  pmodlem2  29961  pmapjoin  29966  pmapjat1  29967  pclfinN  30014  pclfinclN  30064  cdleme50rnlem  30658  diasslssN  31174  dia2dimlem12  31190  dihsslss  31391  baerlem3lem2  31825  baerlem5alem2  31826  baerlem5blem2  31827  hdmaprnN  31982  hgmaprnN  32019
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 2368
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 2374  df-cleq 2380  df-clel 2383  df-in 3270  df-ss 3277
  Copyright terms: Public domain W3C validator