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

Theorem ssrdv 3314
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 3297 . 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 1721    C_ wss 3280
This theorem is referenced by:  sscon  3441  ssdif  3442  unss1  3476  ssrin  3526  eq0rdv  3622  uniss  3996  intss1  4025  intmin  4030  intssuni  4032  iunss1  4064  iinss1  4065  ss2iun  4068  ssiun  4093  ssiun2  4094  iinss  4102  iinss2  4103  trintss  4278  sspwb  4373  pwssun  4449  tron  4564  tz7.7  4567  ssorduni  4725  onint  4734  limsssuc  4789  limuni3  4791  limomss  4809  xpsspw  4945  relop  4982  dmss  5028  dmcosseq  5096  ssrnres  5268  sossfld  5276  dffv2  5755  chfnrn  5800  suppss  5822  dff3  5841  ffnfv  5853  f1imass  5969  fo1stres  6329  fo2ndres  6330  fo2ndf  6412  fnse  6422  reldmtpos  6446  onfununi  6562  smoiun  6582  smorndom  6589  tz7.48-1  6659  tz7.49  6661  oaass  6763  qsss  6924  uniinqs  6943  pmss12g  6999  mapss  7015  ixpssmap2g  7050  ixpssmapg  7051  fineqv  7283  pssnn  7286  ssfii  7382  dffi2  7386  ordtypelem9  7451  ordtypelem10  7452  oismo  7465  unxpwdom2  7512  inf3lemd  7538  inf3lem1  7539  inf3lem6  7544  cantnflem3  7603  cantnf  7605  cnfcom3lem  7616  onssr1  7713  rankunb  7732  tcrank  7764  harcard  7821  carduni  7824  infxpenlem  7851  infpwfien  7899  dfac12r  7982  ackbij2lem1  8055  ackbij1lem18  8073  isfin1-3  8222  fin1a2lem11  8246  fin1a2lem13  8248  zorn2lem4  8335  zorn2lem5  8336  ttukeylem6  8350  ttukeylem7  8351  fpwwe2lem11  8471  fpwwe2lem12  8472  fpwwe2  8474  wunr1om  8550  wunom  8551  tskr1om  8598  tskr1om2  8599  tskxpss  8603  tskcard  8612  tskuni  8614  grothomex  8660  genpss  8837  distrlem1pr  8858  distrlem5pr  8860  prlem934  8866  ltexprlem2  8870  ltexprlem6  8874  ltexprlem7  8875  reclem3pr  8882  reclem4pr  8883  supmul1  9929  supmullem2  9931  peano5uzi  10314  uzss  10462  ixxdisj  10887  ixxss1  10890  ixxss2  10891  ixxss12  10892  ixxub  10893  ixxlb  10894  iocssre  10946  icossre  10947  iccssre  10948  icodisj  10978  fzss1  11047  fzss2  11048  fzosplit  11121  fzouzsplit  11123  sswrd  11692  isercoll  12416  summolem2a  12464  fsumcvg3  12478  fsum2dlem  12509  fsumcom2  12513  qshash  12561  bitsfzo  12902  phimullem  13123  prmreclem5  13243  1arith  13250  vdwlem2  13305  vdwlem6  13309  vdwlem8  13311  ramtlecl  13323  monhom  13916  epihom  13923  funcsetcres2  14203  psdmrn  14594  psssdm2  14602  gsumwspan  14746  frmdss2  14763  ssnmz  14937  conjnmz  14994  gex1  15180  sylow2alem1  15206  sylow3lem3  15218  lsmless1x  15233  lsmless2x  15234  lsmub1x  15235  lsmub2x  15236  lsmmod  15262  lsmdisj2  15269  efgrelexlemb  15337  efgcpbllemb  15342  cntzcmn  15414  gsum2d2  15503  dprdub  15538  dprdss  15542  dprddisj2  15552  ablfacrp  15579  pgpfac1lem3  15590  isdrng2  15800  subrguss  15838  subrgmre  15847  lssssr  15984  lsssssubg  15989  lssmre  15997  lbspss  16109  lspdisj  16152  lbsextlem2  16186  lidl1el  16244  drngnidl  16255  lpiss  16276  unitrrg  16308  fidomndrng  16322  mplbas2  16486  zsssubrg  16712  qsssubdrg  16713  cnsubrg  16714  mulgrhm2  16743  znrrg  16801  ocvocv  16853  ocv2ss  16855  ocvin  16856  lsmcss  16874  cssmre  16875  pjfo  16897  pjcss  16898  obs2ss  16911  bastg  16986  tgss  16988  tgtop  16993  tgidm  17000  en2top  17005  neisspw  17126  topssnei  17143  neiptopuni  17149  lpss3  17163  clslp  17166  tgrest  17177  ssrest  17194  restfpw  17197  restntr  17200  ordtbas2  17209  ordtbas  17210  cnss1  17294  cnss2  17295  cnsscnp  17297  cnrest2r  17305  cmpsublem  17416  cmpsub  17417  tgcmp  17418  cmpcld  17419  hauscmplem  17423  cnconn  17438  2ndcsep  17475  llyss  17495  nllyss  17496  restnlly  17498  restlly  17499  kgenss  17528  kgenidm  17532  llycmpkgen2  17535  1stckgen  17539  kgen2ss  17540  kgencn3  17543  ptbasfi  17566  ptpjopn  17597  ptclsg  17600  txdis  17617  txkgen  17637  xkoptsub  17639  xkopjcn  17641  txcon  17674  qtoptop2  17684  qtopuni  17687  qtopkgen  17695  basqtop  17696  tgqtop  17697  qtopss  17700  qtoprest  17702  qtopomap  17703  qtopcmap  17704  kqsat  17716  kqcldsat  17718  hmphdis  17781  isfild  17843  ssfg  17857  fgss  17858  fgss2  17859  fgfil  17860  fgabs  17864  filcon  17868  fgtr  17875  trfg  17876  uzrest  17882  ufilmax  17892  ufileu  17904  filufint  17905  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem4  17942  flimss2  17957  flimss1  17958  flimclsi  17963  flimcf  17967  flimsncls  17971  fclssscls  18003  fclsss1  18007  fclsss2  18008  fclscf  18010  uffclsflim  18016  alexsublem  18028  alexsubALTlem3  18033  ptcmplem2  18037  ptcmplem3  18038  cnextf  18050  symgtgp  18084  cldsubg  18093  tsmscl  18117  haustsms2  18119  tgptsmscls  18132  tsmsxp  18137  restutop  18220  restutopopn  18221  ustuqtop4  18227  utop2nei  18233  utop3cls  18234  ucncn  18268  xblss2ps  18384  xblss2  18385  unirnblps  18402  unirnbl  18403  xrsblre  18795  xrsmopn  18796  recld2  18798  zdis  18800  icccmplem2  18807  cncfss  18882  cnheiborlem  18932  htpycn  18951  phtpyhtpy  18960  pi1blem  19017  clsocv  19157  cfilfcls  19180  iscmet3lem2  19198  iscmet2  19200  caussi  19203  equivcfil  19205  lmcau  19218  cmetss  19220  pjth  19293  hlhil  19297  ivthicc  19308  ovoliunnul  19356  ovolicopnf  19373  uniioombllem3  19430  dyadmbllem  19444  opnmbllem  19446  volsup2  19450  vitalilem2  19454  itg1addlem4  19544  itg10a  19555  itg1ge0a  19556  mbfi1fseqlem4  19563  itg2gt0  19605  limciun  19734  perfdvf  19743  dvidlem  19755  cpnord  19774  dvaddf  19781  dvmulf  19782  dvcof  19787  dvcj  19789  dvrec  19794  dvcnv  19814  dvlip2  19832  dvivth  19847  dvne0  19848  dvcnvre  19856  ftc1cn  19880  ply1lpir  20054  plyco0  20064  plyexmo  20183  ulmdv  20272  pserdv  20298  abelth  20310  efif1o  20401  logno1  20480  efopnlem2  20501  loglesqr  20595  ppisval  20839  ppisval2  20840  ppinprm  20888  chtnprm  20890  fsumvma  20950  dchrfi  20992  chtppilimlem2  21121  chebbnd2  21124  vmadivsumb  21130  rplogsumlem2  21132  dchrisumlem2  21137  vmalogdivsum2  21185  vmalogdivsum  21186  2vmadivsumlem  21187  selbergb  21196  selberg2b  21199  selberg3lem1  21204  selberg3lem2  21205  selberg3  21206  selberg4lem1  21207  selberg4  21208  pntrlog2bndlem2  21225  pntrlog2bndlem4  21227  sizeusglecusglem1  21446  ococss  22748  shsub1  22779  shless  22814  shmodsi  22844  pjhth  22848  spansnss  23026  spanpr  23035  spansnm0i  23105  pjjsi  23155  sumdmdii  23871  sumdmdlem  23874  sumdmdlem2  23875  cdj3lem1  23890  abrexss  23946  rnmpt2ss  24039  ssnnssfz  24101  kerf1hrm  24215  tpr2rico  24263  esumpcvgval  24421  cldssbrsiga  24494  measdivcstOLD  24531  mbfmcnt  24571  dya2iocuni  24586  lgamcvg2  24792  sconpi1  24879  cvmscld  24913  cvmsss2  24914  cvmliftlem15  24938  rtrclreclem.trans  25099  prodmolem2a  25213  fprod2dlem  25257  fprodcom2  25261  dfon2lem6  25358  predpo  25398  preddowncl  25410  wfrlem10  25479  nofulllem5  25574  supaddc  26137  supadd  26138  mblfinlem  26143  ftc1cnnc  26178  fnessref  26263  locfincmp  26274  locfincf  26276  fgmin  26289  tailfb  26296  sstotbnd3  26375  prdstotbnd  26393  cntotbnd  26395  ismtyhmeo  26404  1idl  26526  eldiophss  26723  rencldnfilem  26771  pellexlem5  26786  pell14qrss1234  26809  pell1qrss14  26821  pellfundre  26834  pellfundge  26835  pellfundlb  26837  pellfundglb  26838  harinf  26995  kercvrlsm  27049  pwssplit4  27059  frlmsslsp  27116  lindfrn  27159  hbtlem5  27200  proot1hash  27387  refsumcn  27568  stoweidlem27  27643  stoweidlem46  27662  stoweidlem57  27673  ffnafv  27902  trsspwALT3  28642  sspwimpALT2  28750  bnj1033  29044  bnj1398  29109  lshpdisj  29470  lssats  29495  lkrlsp  29585  lkrin  29647  glbconxN  29860  paddss1  30299  paddss2  30300  paddasslem16  30317  paddidm  30323  pmodlem2  30329  pmapjoin  30334  pmapjat1  30335  pclfinN  30382  pclfinclN  30432  cdleme50rnlem  31026  diasslssN  31542  dia2dimlem12  31558  dihsslss  31759  baerlem3lem2  32193  baerlem5alem2  32194  baerlem5blem2  32195  hdmaprnN  32350  hgmaprnN  32387
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
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 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator