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

Theorem ssrdv 3354
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 1641 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3337 . 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 1549    e. wcel 1725    C_ wss 3320
This theorem is referenced by:  sscon  3481  ssdif  3482  unss1  3516  ssrin  3566  eq0rdv  3662  uniss  4036  intss1  4065  intmin  4070  intssuni  4072  iunss1  4104  iinss1  4105  ss2iun  4108  ssiun  4133  ssiun2  4134  iinss  4142  iinss2  4143  trintss  4318  sspwb  4413  pwssun  4489  tron  4604  tz7.7  4607  ssorduni  4766  onint  4775  limsssuc  4830  limuni3  4832  limomss  4850  xpsspw  4986  relop  5023  dmss  5069  dmcosseq  5137  ssrnres  5309  sossfld  5317  dffv2  5796  chfnrn  5841  suppss  5863  dff3  5882  ffnfv  5894  f1imass  6010  fo1stres  6370  fo2ndres  6371  fo2ndf  6453  fnse  6463  reldmtpos  6487  onfununi  6603  smoiun  6623  smorndom  6630  tz7.48-1  6700  tz7.49  6702  oaass  6804  qsss  6965  uniinqs  6984  pmss12g  7040  mapss  7056  ixpssmap2g  7091  ixpssmapg  7092  fineqv  7324  pssnn  7327  ssfii  7424  dffi2  7428  ordtypelem9  7495  ordtypelem10  7496  oismo  7509  unxpwdom2  7556  inf3lemd  7582  inf3lem1  7583  inf3lem6  7588  cantnflem3  7647  cantnf  7649  cnfcom3lem  7660  onssr1  7757  rankunb  7776  tcrank  7808  harcard  7865  carduni  7868  infxpenlem  7895  infpwfien  7943  dfac12r  8026  ackbij2lem1  8099  ackbij1lem18  8117  isfin1-3  8266  fin1a2lem11  8290  fin1a2lem13  8292  zorn2lem4  8379  zorn2lem5  8380  ttukeylem6  8394  ttukeylem7  8395  fpwwe2lem11  8515  fpwwe2lem12  8516  fpwwe2  8518  wunr1om  8594  wunom  8595  tskr1om  8642  tskr1om2  8643  tskxpss  8647  tskcard  8656  tskuni  8658  grothomex  8704  genpss  8881  distrlem1pr  8902  distrlem5pr  8904  prlem934  8910  ltexprlem2  8914  ltexprlem6  8918  ltexprlem7  8919  reclem3pr  8926  reclem4pr  8927  supmul1  9973  supmullem2  9975  peano5uzi  10358  uzss  10506  ixxdisj  10931  ixxss1  10934  ixxss2  10935  ixxss12  10936  ixxub  10937  ixxlb  10938  iocssre  10990  icossre  10991  iccssre  10992  icodisj  11022  fzss1  11091  fzss2  11092  fzosplit  11166  fzouzsplit  11168  sswrd  11737  isercoll  12461  summolem2a  12509  fsumcvg3  12523  fsum2dlem  12554  fsumcom2  12558  qshash  12606  bitsfzo  12947  phimullem  13168  prmreclem5  13288  1arith  13295  vdwlem2  13350  vdwlem6  13354  vdwlem8  13356  ramtlecl  13368  monhom  13961  epihom  13968  funcsetcres2  14248  psdmrn  14639  psssdm2  14647  gsumwspan  14791  frmdss2  14808  ssnmz  14982  conjnmz  15039  gex1  15225  sylow2alem1  15251  sylow3lem3  15263  lsmless1x  15278  lsmless2x  15279  lsmub1x  15280  lsmub2x  15281  lsmmod  15307  lsmdisj2  15314  efgrelexlemb  15382  efgcpbllemb  15387  cntzcmn  15459  gsum2d2  15548  dprdub  15583  dprdss  15587  dprddisj2  15597  ablfacrp  15624  pgpfac1lem3  15635  isdrng2  15845  subrguss  15883  subrgmre  15892  lssssr  16029  lsssssubg  16034  lssmre  16042  lbspss  16154  lspdisj  16197  lbsextlem2  16231  lidl1el  16289  drngnidl  16300  lpiss  16321  unitrrg  16353  fidomndrng  16367  mplbas2  16531  zsssubrg  16757  qsssubdrg  16758  cnsubrg  16759  mulgrhm2  16788  znrrg  16846  ocvocv  16898  ocv2ss  16900  ocvin  16901  lsmcss  16919  cssmre  16920  pjfo  16942  pjcss  16943  obs2ss  16956  bastg  17031  tgss  17033  tgtop  17038  tgidm  17045  en2top  17050  neisspw  17171  topssnei  17188  neiptopuni  17194  lpss3  17208  clslp  17212  tgrest  17223  ssrest  17240  restfpw  17243  restntr  17246  ordtbas2  17255  ordtbas  17256  cnss1  17340  cnss2  17341  cnsscnp  17343  cnrest2r  17351  cmpsublem  17462  cmpsub  17463  tgcmp  17464  cmpcld  17465  hauscmplem  17469  cnconn  17485  2ndcsep  17522  llyss  17542  nllyss  17543  restnlly  17545  restlly  17546  kgenss  17575  kgenidm  17579  llycmpkgen2  17582  1stckgen  17586  kgen2ss  17587  kgencn3  17590  ptbasfi  17613  ptpjopn  17644  ptclsg  17647  txdis  17664  txkgen  17684  xkoptsub  17686  xkopjcn  17688  txcon  17721  qtoptop2  17731  qtopuni  17734  qtopkgen  17742  basqtop  17743  tgqtop  17744  qtopss  17747  qtoprest  17749  qtopomap  17750  qtopcmap  17751  kqsat  17763  kqcldsat  17765  hmphdis  17828  isfild  17890  ssfg  17904  fgss  17905  fgss2  17906  fgfil  17907  fgabs  17911  filcon  17915  fgtr  17922  trfg  17923  uzrest  17929  ufilmax  17939  ufileu  17951  filufint  17952  rnelfm  17985  fmfnfmlem2  17987  fmfnfmlem4  17989  flimss2  18004  flimss1  18005  flimclsi  18010  flimcf  18014  flimsncls  18018  fclssscls  18050  fclsss1  18054  fclsss2  18055  fclscf  18057  uffclsflim  18063  alexsublem  18075  alexsubALTlem3  18080  ptcmplem2  18084  ptcmplem3  18085  cnextf  18097  symgtgp  18131  cldsubg  18140  tsmscl  18164  haustsms2  18166  tgptsmscls  18179  tsmsxp  18184  restutop  18267  restutopopn  18268  ustuqtop4  18274  utop2nei  18280  utop3cls  18281  ucncn  18315  xblss2ps  18431  xblss2  18432  unirnblps  18449  unirnbl  18450  xrsblre  18842  xrsmopn  18843  recld2  18845  zdis  18847  icccmplem2  18854  cncfss  18929  cnheiborlem  18979  htpycn  18998  phtpyhtpy  19007  pi1blem  19064  clsocv  19204  cfilfcls  19227  iscmet3lem2  19245  iscmet2  19247  caussi  19250  equivcfil  19252  lmcau  19265  cmetss  19267  pjth  19340  hlhil  19344  ivthicc  19355  ovoliunnul  19403  ovolicopnf  19420  uniioombllem3  19477  dyadmbllem  19491  opnmbllem  19493  volsup2  19497  vitalilem2  19501  itg1addlem4  19591  itg10a  19602  itg1ge0a  19603  mbfi1fseqlem4  19610  itg2gt0  19652  limciun  19781  perfdvf  19790  dvidlem  19802  cpnord  19821  dvaddf  19828  dvmulf  19829  dvcof  19834  dvcj  19836  dvrec  19841  dvcnv  19861  dvlip2  19879  dvivth  19894  dvne0  19895  dvcnvre  19903  ftc1cn  19927  ply1lpir  20101  plyco0  20111  plyexmo  20230  ulmdv  20319  pserdv  20345  abelth  20357  efif1o  20448  logno1  20527  efopnlem2  20548  loglesqr  20642  ppisval  20886  ppisval2  20887  ppinprm  20935  chtnprm  20937  fsumvma  20997  dchrfi  21039  chtppilimlem2  21168  chebbnd2  21171  vmadivsumb  21177  rplogsumlem2  21179  dchrisumlem2  21184  vmalogdivsum2  21232  vmalogdivsum  21233  2vmadivsumlem  21234  selbergb  21243  selberg2b  21246  selberg3lem1  21251  selberg3lem2  21252  selberg3  21253  selberg4lem1  21254  selberg4  21255  pntrlog2bndlem2  21272  pntrlog2bndlem4  21274  sizeusglecusglem1  21493  ococss  22795  shsub1  22826  shless  22861  shmodsi  22891  pjhth  22895  spansnss  23073  spanpr  23082  spansnm0i  23152  pjjsi  23202  sumdmdii  23918  sumdmdlem  23921  sumdmdlem2  23922  cdj3lem1  23937  abrexss  23993  rnmpt2ss  24086  ssnnssfz  24148  kerf1hrm  24262  tpr2rico  24310  esumpcvgval  24468  cldssbrsiga  24541  measdivcstOLD  24578  mbfmcnt  24618  dya2iocuni  24633  lgamcvg2  24839  sconpi1  24926  cvmscld  24960  cvmsss2  24961  cvmliftlem15  24985  rtrclreclem.trans  25146  prodmolem2a  25260  fprod2dlem  25304  fprodcom2  25308  dfon2lem6  25415  predpo  25459  preddowncl  25471  wfrlem10  25547  nofulllem5  25661  supaddc  26237  supadd  26238  opnmbllem0  26242  ftc1cnnc  26279  fnessref  26373  locfincmp  26384  locfincf  26386  fgmin  26399  tailfb  26406  sstotbnd3  26485  prdstotbnd  26503  cntotbnd  26505  ismtyhmeo  26514  1idl  26636  eldiophss  26833  rencldnfilem  26881  pellexlem5  26896  pell14qrss1234  26919  pell1qrss14  26931  pellfundre  26944  pellfundge  26945  pellfundlb  26947  pellfundglb  26948  harinf  27105  kercvrlsm  27158  pwssplit4  27168  frlmsslsp  27225  lindfrn  27268  hbtlem5  27309  proot1hash  27496  refsumcn  27677  stoweidlem27  27752  stoweidlem46  27771  stoweidlem57  27782  ffnafv  28011  trsspwALT3  28933  sspwimpALT2  29040  bnj1033  29338  bnj1398  29403  lshpdisj  29785  lssats  29810  lkrlsp  29900  lkrin  29962  glbconxN  30175  paddss1  30614  paddss2  30615  paddasslem16  30632  paddidm  30638  pmodlem2  30644  pmapjoin  30649  pmapjat1  30650  pclfinN  30697  pclfinclN  30747  cdleme50rnlem  31341  diasslssN  31857  dia2dimlem12  31873  dihsslss  32074  baerlem3lem2  32508  baerlem5alem2  32509  baerlem5blem2  32510  hdmaprnN  32665  hgmaprnN  32702
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator