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

Theorem ssrdv 3198
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 1621 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3182 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
42, 3sylibr 203 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530    e. wcel 1696    C_ wss 3165
This theorem is referenced by:  sscon  3323  ssdif  3324  unss1  3357  ssrin  3407  eq0rdv  3502  uniss  3864  intss1  3893  intmin  3898  intssuni  3900  iunss1  3932  iinss1  3933  ss2iun  3936  ssiun  3960  ssiun2  3961  iinss  3969  iinss2  3970  trintss  4145  sspwb  4239  pwssun  4315  tron  4431  tz7.7  4434  ssorduni  4593  onint  4602  limsssuc  4657  limuni3  4659  limomss  4677  xpsspw  4813  relop  4850  dmss  4894  dmcosseq  4962  ssrnres  5132  sossfld  5136  dffv2  5608  chfnrn  5652  suppss  5674  dff3  5689  ffnfv  5701  f1imass  5804  fo1stres  6159  fo2ndres  6160  fnse  6248  reldmtpos  6258  onfununi  6374  smoiun  6394  smorndom  6401  tz7.48-1  6471  tz7.49  6473  oaass  6575  qsss  6736  pmss12g  6810  mapss  6826  ixpssmap2g  6861  ixpssmapg  6862  fineqv  7094  pssnn  7097  ssfii  7188  dffi2  7192  ordtypelem9  7257  ordtypelem10  7258  oismo  7271  unxpwdom2  7318  inf3lemd  7344  inf3lem1  7345  inf3lem6  7350  cantnflem3  7409  cantnf  7411  cnfcom3lem  7422  onssr1  7519  rankunb  7538  tcrank  7570  harcard  7627  carduni  7630  infxpenlem  7657  infpwfien  7705  dfac12r  7788  ackbij2lem1  7861  ackbij1lem18  7879  isfin1-3  8028  fin1a2lem11  8052  fin1a2lem13  8054  zorn2lem4  8142  zorn2lem5  8143  ttukeylem6  8157  ttukeylem7  8158  fpwwe2lem11  8278  fpwwe2lem12  8279  fpwwe2  8281  wunr1om  8357  wunom  8358  tskr1om  8405  tskr1om2  8406  tskxpss  8410  tskcard  8419  tskuni  8421  grothomex  8467  genpss  8644  distrlem1pr  8665  distrlem5pr  8667  prlem934  8673  ltexprlem2  8677  ltexprlem6  8681  ltexprlem7  8682  reclem3pr  8689  reclem4pr  8690  supmul1  9735  supmullem2  9737  peano5uzi  10116  uzss  10264  ixxdisj  10687  ixxss1  10690  ixxss2  10691  ixxss12  10692  ixxub  10693  ixxlb  10694  iocssre  10745  icossre  10746  iccssre  10747  icodisj  10777  fzss1  10846  fzss2  10847  fzosplit  10915  fzouzsplit  10917  sswrd  11439  isercoll  12157  summolem2a  12204  fsumcvg3  12218  fsum2dlem  12249  fsumcom2  12253  qshash  12301  bitsfzo  12642  phimullem  12863  prmreclem5  12983  1arith  12990  vdwlem2  13045  vdwlem6  13049  vdwlem8  13051  ramtlecl  13063  monhom  13654  epihom  13661  funcsetcres2  13941  psdmrn  14332  psssdm2  14340  gsumwspan  14484  frmdss2  14501  ssnmz  14675  conjnmz  14732  gex1  14918  sylow2alem1  14944  sylow3lem3  14956  lsmless1x  14971  lsmless2x  14972  lsmub1x  14973  lsmub2x  14974  lsmmod  15000  lsmdisj2  15007  efgrelexlemb  15075  efgcpbllemb  15080  cntzcmn  15152  gsum2d2  15241  dprdub  15276  dprdss  15280  dprddisj2  15290  ablfacrp  15317  pgpfac1lem3  15328  isdrng2  15538  subrguss  15576  subrgmre  15585  lssssr  15726  lsssssubg  15731  lssmre  15739  lbspss  15851  lspdisj  15894  lbsextlem2  15928  lidl1el  15986  drngnidl  15997  lpiss  16018  unitrrg  16050  fidomndrng  16064  mplbas2  16228  zsssubrg  16446  qsssubdrg  16447  cnsubrg  16448  mulgrhm2  16477  znrrg  16535  ocvocv  16587  ocv2ss  16589  ocvin  16590  lsmcss  16608  cssmre  16609  pjfo  16631  pjcss  16632  obs2ss  16645  bastg  16720  tgss  16722  tgtop  16727  tgidm  16734  en2top  16739  neisspw  16860  topssnei  16877  lpss3  16892  clslp  16895  tgrest  16906  ssrest  16923  restfpw  16926  restntr  16928  ordtbas2  16937  ordtbas  16938  cnss1  17021  cnss2  17022  cnsscnp  17024  cnrest2r  17031  cmpsublem  17142  cmpsub  17143  tgcmp  17144  cmpcld  17145  hauscmplem  17149  cnconn  17164  2ndcsep  17201  llyss  17221  nllyss  17222  restnlly  17224  restlly  17225  kgenss  17254  kgenidm  17258  llycmpkgen2  17261  1stckgen  17265  kgen2ss  17266  kgencn3  17269  ptbasfi  17292  ptpjopn  17322  ptclsg  17325  txdis  17342  txkgen  17362  xkoptsub  17364  xkopjcn  17366  txcon  17399  qtoptop2  17406  qtopuni  17409  qtopkgen  17417  basqtop  17418  tgqtop  17419  qtopss  17422  qtoprest  17424  qtopomap  17425  qtopcmap  17426  kqsat  17438  kqcldsat  17440  hmphdis  17503  isfild  17569  ssfg  17583  fgss  17584  fgss2  17585  fgfil  17586  fgabs  17590  filcon  17594  fgtr  17601  trfg  17602  uzrest  17608  ufilmax  17618  ufileu  17630  filufint  17631  rnelfm  17664  fmfnfmlem2  17666  fmfnfmlem4  17668  flimss2  17683  flimss1  17684  flimclsi  17689  flimcf  17693  flimsncls  17697  fclssscls  17729  fclsss1  17733  fclsss2  17734  fclscf  17736  uffclsflim  17742  alexsublem  17754  alexsubALTlem3  17759  ptcmplem2  17763  ptcmplem3  17764  symgtgp  17800  cldsubg  17809  tsmscl  17833  haustsms2  17835  tgptsmscls  17848  tsmsxp  17853  xblss2  17974  unirnbl  17985  xrsblre  18333  xrsmopn  18334  recld2  18336  zdis  18338  icccmplem2  18344  cncfss  18419  cnheiborlem  18468  htpycn  18487  phtpyhtpy  18496  pi1blem  18553  clsocv  18693  cfilfcls  18716  iscmet3lem2  18734  iscmet2  18736  caussi  18739  equivcfil  18741  lmcau  18754  cmetss  18756  pjth  18819  hlhil  18823  ivthicc  18834  ovoliunnul  18882  ovolicopnf  18899  uniioombllem3  18956  dyadmbllem  18970  opnmbllem  18972  volsup2  18976  vitalilem2  18980  itg1addlem4  19070  itg10a  19081  itg1ge0a  19082  mbfi1fseqlem4  19089  itg2gt0  19131  limciun  19260  perfdvf  19269  dvidlem  19281  cpnord  19300  dvaddf  19307  dvmulf  19308  dvcof  19313  dvcj  19315  dvrec  19320  dvcnv  19340  dvlip2  19358  dvivth  19373  dvne0  19374  dvcnvre  19382  ftc1cn  19406  ply1lpir  19580  plyco0  19590  plyexmo  19709  ulmdv  19796  pserdv  19821  abelth  19833  efif1o  19924  logno1  19999  efopnlem2  20020  loglesqr  20114  ppisval  20357  ppisval2  20358  ppinprm  20406  chtnprm  20408  fsumvma  20468  dchrfi  20510  chtppilimlem2  20639  chebbnd2  20642  vmadivsumb  20648  rplogsumlem2  20650  dchrisumlem2  20655  vmalogdivsum2  20703  vmalogdivsum  20704  2vmadivsumlem  20705  selbergb  20714  selberg2b  20717  selberg3lem1  20722  selberg3lem2  20723  selberg3  20724  selberg4lem1  20725  selberg4  20726  pntrlog2bndlem2  20743  pntrlog2bndlem4  20745  ococss  21888  shsub1  21919  shless  21954  shmodsi  21984  pjhth  21988  spansnss  22166  spanpr  22175  spansnm0i  22245  pjjsi  22295  sumdmdii  23011  sumdmdlem  23014  sumdmdlem2  23015  cdj3lem1  23030  abrexss  23056  ssnnssfz  23292  tpr2rico  23311  esumpcvgval  23461  cldssbrsiga  23533  measdivcstOLD  23566  measdivcst  23567  mbfmcnt  23588  sconpi1  23785  cvmscld  23819  cvmsss2  23820  cvmliftlem15  23844  rtrclreclem.trans  24058  prodmolem2a  24157  dfon2lem6  24215  predpo  24255  preddowncl  24267  wfrlem10  24336  nofulllem5  24431  supaddc  24995  supadd  24996  ftc1cnnc  25025  uninqs  25142  domintrefc  25228  iccss3  25237  npincppr  25262  nsn  25633  limfn  25668  islimrs3  25684  islimrs4  25685  icccon2  25803  icccon3  25804  icccon4  25805  rdmob  25851  rcmob  25852  tareltsuc  26001  fnctartar  26010  fnctartar2  26011  segline  26244  pxysxy  26245  fnessref  26396  locfincmp  26407  locfincf  26409  fgmin  26422  tailfb  26429  lpss2  26571  sstotbnd3  26603  prdstotbnd  26621  cntotbnd  26623  ismtyhmeo  26632  1idl  26754  eldiophss  26957  rencldnfilem  27006  pellexlem5  27021  pell14qrss1234  27044  pell1qrss14  27056  pellfundre  27069  pellfundge  27070  pellfundlb  27072  pellfundglb  27073  harinf  27230  kercvrlsm  27284  pwssplit4  27294  frlmsslsp  27351  lindfrn  27394  hbtlem5  27435  proot1hash  27622  refsumcn  27804  stoweidlem27  27879  stoweidlem46  27898  stoweidlem57  27909  ffnafv  28139  trsspwALT3  28910  bnj1033  29315  bnj1398  29380  lshpdisj  29799  lssats  29824  lkrlsp  29914  lkrin  29976  glbconxN  30189  paddss1  30628  paddss2  30629  paddasslem16  30646  paddidm  30652  pmodlem2  30658  pmapjoin  30663  pmapjat1  30664  pclfinN  30711  pclfinclN  30761  cdleme50rnlem  31355  diasslssN  31871  dia2dimlem12  31887  dihsslss  32088  baerlem3lem2  32522  baerlem5alem2  32523  baerlem5blem2  32524  hdmaprnN  32679  hgmaprnN  32716
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator