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

Theorem ssrdv 3460
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 1686 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3443 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
42, 3sylibr 212 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1368    e. wcel 1758    C_ wss 3426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3433  df-ss 3440
This theorem is referenced by:  sscon  3588  ssdif  3589  unss1  3623  ssrin  3673  eq0rdv  3770  uniss  4210  intss1  4241  intmin  4246  intssuni  4248  iunss1  4280  iinss1  4281  ss2iun  4284  ssiun  4310  ssiun2  4311  iinss  4319  iinss2  4320  trintss  4499  sspwb  4639  pwssun  4725  tron  4840  tz7.7  4843  xpsspw  5051  relop  5088  dmss  5137  dmcosseq  5199  ssrnres  5374  sossfld  5383  dffv2  5863  chfnrn  5913  suppssOLD  5935  dff3  5955  ffnfv  5968  f1imass  6076  ssorduni  6497  onint  6506  limsssuc  6561  limuni3  6563  limomss  6581  fo1stres  6700  fo2ndres  6701  fo2ndf  6779  fnse  6789  ressuppssdif  6810  suppss  6819  reldmtpos  6853  onfununi  6902  smoiun  6922  smorndom  6929  tz7.48-1  6998  tz7.49  7000  oaass  7100  qsss  7261  uniinqs  7280  pmss12g  7339  mapss  7355  ixpssmap2g  7392  ixpssmapg  7393  fineqv  7629  pssnn  7632  ssfii  7770  dffi2  7774  ordtypelem9  7841  ordtypelem10  7842  oismo  7855  unxpwdom2  7904  inf3lemd  7934  inf3lem1  7935  inf3lem6  7940  cantnflem3  8000  cantnf  8002  cantnflem3OLD  8022  cantnfOLD  8024  cnfcom3lem  8037  cnfcom3lemOLD  8045  onssr1  8139  rankunb  8158  tcrank  8192  harcard  8249  carduni  8252  infxpenlem  8281  infpwfien  8333  dfac12r  8416  ackbij2lem1  8489  ackbij1lem18  8507  isfin1-3  8656  fin1a2lem11  8680  fin1a2lem13  8682  zorn2lem4  8769  zorn2lem5  8770  ttukeylem6  8784  ttukeylem7  8785  fpwwe2lem11  8908  fpwwe2lem12  8909  fpwwe2  8911  wunr1om  8987  wunom  8988  tskr1om  9035  tskr1om2  9036  tskxpss  9040  tskcard  9049  tskuni  9051  grothomex  9097  genpss  9274  distrlem1pr  9295  distrlem5pr  9297  prlem934  9303  ltexprlem2  9307  ltexprlem6  9311  ltexprlem7  9312  reclem3pr  9319  reclem4pr  9320  supmul1  10396  supmullem2  10398  peano5uzi  10831  uzss  10982  ixxdisj  11416  ixxss1  11419  ixxss2  11420  ixxss12  11421  ixxub  11422  ixxlb  11423  iocssre  11476  icossre  11477  iccssre  11478  icodisj  11511  fzss1  11598  fzss2  11599  fzosplit  11683  fzouzsplit  11685  ssfzo12bi  11723  sswrd  12344  isercoll  13247  summolem2a  13294  fsumcvg3  13308  fsum2dlem  13339  fsumcom2  13343  qshash  13392  bitsfzo  13733  phimullem  13956  prmreclem5  14083  1arith  14090  vdwlem2  14145  vdwlem6  14149  vdwlem8  14151  ramtlecl  14163  monhom  14776  epihom  14783  funcsetcres2  15063  psdmrn  15479  psssdm2  15487  gsumwspan  15626  frmdss2  15643  ssnmz  15825  conjnmz  15882  gex1  16194  sylow2alem1  16220  sylow3lem3  16232  lsmless1x  16247  lsmless2x  16248  lsmub1x  16249  lsmub2x  16250  lsmmod  16276  lsmdisj2  16283  efgrelexlemb  16351  efgcpbllemb  16356  cntzcmn  16428  gsum2d2  16571  dprdub  16627  dprdss  16631  dprddisj2  16642  dprddisj2OLD  16643  ablfacrp  16672  pgpfac1lem3  16683  kerf1hrm  16937  isdrng2  16948  subrguss  16986  subrgmre  16995  lssssr  17140  lsssssubg  17145  lssmre  17153  lbspss  17269  lspdisj  17312  lbsextlem2  17346  lidl1el  17406  drngnidl  17417  lpiss  17438  unitrrg  17471  fidomndrng  17485  mplbas2  17658  mplbas2OLD  17659  zsssubrg  17980  qsssubdrg  17981  cnsubrg  17982  mulgrhm2  18036  mulgrhm2OLD  18039  znrrg  18107  ocvocv  18205  ocv2ss  18207  ocvin  18208  lsmcss  18226  cssmre  18227  pjfo  18249  pjcss  18250  obs2ss  18263  frlmsslsp  18332  frlmsslspOLD  18333  lindfrn  18359  bastg  18687  tgss  18689  tgtop  18694  tgidm  18701  en2top  18706  neisspw  18827  topssnei  18844  neiptopuni  18850  lpss3  18864  clslp  18868  tgrest  18879  ssrest  18896  restfpw  18899  restntr  18902  ordtbas2  18911  ordtbas  18912  cnss1  18996  cnss2  18997  cnsscnp  18999  cnrest2r  19007  cmpsublem  19118  cmpsub  19119  tgcmp  19120  cmpcld  19121  hauscmplem  19125  cnconn  19142  2ndcsep  19179  llyss  19199  nllyss  19200  restnlly  19202  restlly  19203  kgenss  19232  kgenidm  19236  llycmpkgen2  19239  1stckgen  19243  kgen2ss  19244  kgencn3  19247  ptbasfi  19270  ptpjopn  19301  ptclsg  19304  txdis  19321  txkgen  19341  xkoptsub  19343  xkopjcn  19345  txcon  19378  qtoptop2  19388  qtopuni  19391  qtopkgen  19399  basqtop  19400  tgqtop  19401  qtopss  19404  qtoprest  19406  qtopomap  19407  qtopcmap  19408  kqsat  19420  kqcldsat  19422  hmphdis  19485  isfild  19547  ssfg  19561  fgss  19562  fgss2  19563  fgfil  19564  fgabs  19568  filcon  19572  fgtr  19579  trfg  19580  uzrest  19586  ufilmax  19596  ufileu  19608  filufint  19609  rnelfm  19642  fmfnfmlem2  19644  fmfnfmlem4  19646  flimss2  19661  flimss1  19662  flimclsi  19667  flimcf  19671  flimsncls  19675  fclssscls  19707  fclsss1  19711  fclsss2  19712  fclscf  19714  uffclsflim  19720  alexsublem  19732  alexsubALTlem3  19737  ptcmplem2  19741  ptcmplem3  19742  cnextf  19754  symgtgp  19788  cldsubg  19797  tsmscl  19821  haustsms2  19823  tgptsmscls  19840  tsmsxp  19845  restutop  19928  restutopopn  19929  ustuqtop4  19935  utop2nei  19941  utop3cls  19942  ucncn  19976  xblss2ps  20092  xblss2  20093  unirnblps  20110  unirnbl  20111  xrsblre  20504  xrsmopn  20505  recld2  20507  zdis  20509  icccmplem2  20516  cncfss  20591  cnheiborlem  20642  htpycn  20661  phtpyhtpy  20670  pi1blem  20727  clsocv  20878  cfilfcls  20901  iscmet3lem2  20919  iscmet2  20921  caussi  20924  equivcfil  20926  lmcau  20939  cmetss  20941  pjth  21042  hlhil  21046  ivthicc  21058  ovoliunnul  21106  ovolicopnf  21123  uniioombllem3  21181  dyadmbllem  21195  opnmbllem  21197  volsup2  21201  vitalilem2  21205  itg1addlem4  21293  itg10a  21304  itg1ge0a  21305  mbfi1fseqlem4  21312  itg2gt0  21354  limciun  21485  perfdvf  21494  dvidlem  21506  cpnord  21525  dvaddf  21532  dvmulf  21533  dvcof  21538  dvcj  21540  dvrec  21545  dvcnv  21565  dvlip2  21583  dvivth  21598  dvne0  21599  dvcnvre  21607  ftc1cn  21631  ply1lpir  21766  plyco0  21776  plyexmo  21895  ulmdv  21984  pserdv  22010  abelth  22022  efif1o  22118  logno1  22197  efopnlem2  22218  loglesqr  22312  ppisval  22557  ppisval2  22558  ppinprm  22606  chtnprm  22608  fsumvma  22668  dchrfi  22710  chtppilimlem2  22839  chebbnd2  22842  vmadivsumb  22848  rplogsumlem2  22850  dchrisumlem2  22855  vmalogdivsum2  22903  vmalogdivsum  22904  2vmadivsumlem  22905  selbergb  22914  selberg2b  22917  selberg3lem1  22922  selberg3lem2  22923  selberg3  22924  selberg4lem1  22925  selberg4  22926  pntrlog2bndlem2  22943  pntrlog2bndlem4  22945  sizeusglecusglem1  23527  ococss  24831  shsub1  24862  shless  24897  shmodsi  24927  pjhth  24931  spansnss  25109  spanpr  25118  spansnm0i  25188  pjjsi  25238  sumdmdii  25954  sumdmdlem  25957  sumdmdlem2  25958  cdj3lem1  25973  abrexss  26028  rnmpt2ss  26126  unifi3  26139  ssnnssfz  26210  tpr2rico  26476  esumpcvgval  26661  cldssbrsiga  26735  measdivcstOLD  26772  mbfmcnt  26817  dya2iocuni  26832  oddpwdc  26871  eulerpartlemgs2  26897  lgamcvg2  27175  sconpi1  27262  cvmscld  27296  cvmsss2  27297  cvmliftlem15  27321  rtrclreclem.trans  27482  prodmolem2a  27581  fprod2dlem  27625  fprodcom2  27629  dfon2lem6  27735  predpo  27779  preddowncl  27791  wfrlem10  27867  nofulllem5  27981  supaddc  28555  supadd  28556  opnmbllem0  28565  ftc1cnnc  28604  fnessref  28703  locfincmp  28714  locfincf  28716  fgmin  28729  tailfb  28736  sstotbnd3  28813  prdstotbnd  28831  cntotbnd  28833  ismtyhmeo  28842  1idl  28964  eldiophss  29251  rencldnfilem  29297  pellexlem5  29312  pell14qrss1234  29335  pell1qrss14  29347  pellfundre  29360  pellfundge  29361  pellfundlb  29363  pellfundglb  29364  harinf  29521  kercvrlsm  29574  pwssplit4  29580  hbtlem5  29622  proot1hash  29706  refsumcn  29890  stoweidlem27  29960  stoweidlem46  29979  stoweidlem57  29990  ffnafv  30215  ssnn0ssfz  30879  suppssfz  30924  fsuppmapnn0fiub  30937  scmatsgrp1  31043  lincolss  31075  lcoss  31077  lcosslsp  31079  m2cpmrngiso  31217  m2cpminv  31222  trsspwALT3  31854  sspwimpALT2  31964  bnj1033  32260  bnj1398  32325  lshpdisj  32938  lssats  32963  lkrlsp  33053  lkrin  33115  glbconxN  33328  paddss1  33767  paddss2  33768  paddasslem16  33785  paddidm  33791  pmodlem2  33797  pmapjoin  33802  pmapjat1  33803  pclfinN  33850  pclfinclN  33900  cdleme50rnlem  34494  diasslssN  35010  dia2dimlem12  35026  dihsslss  35227  baerlem3lem2  35661  baerlem5alem2  35662  baerlem5blem2  35663  hdmaprnN  35818  hgmaprnN  35855
  Copyright terms: Public domain W3C validator