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

Theorem ssrdv 3495
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 1724 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3478 . 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 1396    e. wcel 1823    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  sscon  3624  ssdif  3625  unss1  3659  ssrin  3709  eq0rdv  3819  uniss  4256  intss1  4286  intmin  4291  intssuni  4294  iunss1  4327  iinss1  4328  ss2iun  4331  ssiun  4357  ssiun2  4358  iinss  4366  iinss2  4367  trintss  4548  sspwb  4686  pwssun  4775  tron  4890  tz7.7  4893  xpsspw  5104  relop  5142  dmss  5191  dmcosseq  5253  ssrnres  5430  sossfld  5438  dffv2  5921  chfnrn  5974  suppssOLD  5996  fvn0ssdmfun  5998  fveqdmss  6002  dff3  6020  ffnfv  6033  f1imass  6147  ssorduni  6594  onint  6603  limsssuc  6658  limuni3  6660  limomss  6678  fo1stres  6797  fo2ndres  6798  fo2ndf  6880  fnse  6890  ressuppssdif  6913  suppss  6922  reldmtpos  6955  onfununi  7004  smoiun  7024  smorndom  7031  tz7.48-1  7100  tz7.49  7102  oaass  7202  qsss  7364  uniinqs  7383  pmss12g  7438  mapss  7454  ixpssmap2g  7491  ixpssmapg  7492  fineqv  7728  pssnn  7731  ssfii  7871  dffi2  7875  ordtypelem9  7943  ordtypelem10  7944  oismo  7957  unxpwdom2  8006  inf3lemd  8035  inf3lem1  8036  inf3lem6  8041  cantnflem3  8101  cantnf  8103  cantnflem3OLD  8123  cantnfOLD  8125  cnfcom3lem  8138  cnfcom3lemOLD  8146  onssr1  8240  rankunb  8259  tcrank  8293  harcard  8350  carduni  8353  infxpenlem  8382  infpwfien  8434  dfac12r  8517  ackbij2lem1  8590  ackbij1lem18  8608  isfin1-3  8757  fin1a2lem11  8781  fin1a2lem13  8783  zorn2lem4  8870  zorn2lem5  8871  ttukeylem6  8885  ttukeylem7  8886  fpwwe2lem11  9007  fpwwe2lem12  9008  fpwwe2  9010  wunr1om  9086  wunom  9087  tskr1om  9134  tskr1om2  9135  tskxpss  9139  tskcard  9148  tskuni  9150  grothomex  9196  genpss  9371  distrlem1pr  9392  distrlem5pr  9394  prlem934  9400  ltexprlem2  9404  ltexprlem6  9408  ltexprlem7  9409  reclem3pr  9416  reclem4pr  9417  supmul1  10503  supmullem2  10505  peano5uzi  10947  uzss  11102  ixxdisj  11547  ixxss1  11550  ixxss2  11551  ixxss12  11552  ixxub  11553  ixxlb  11554  iocssre  11607  icossre  11608  iccssre  11609  icodisj  11648  fzss1  11726  fzss2  11727  fzosplit  11835  fzouzsplit  11837  ssfzo12bi  11888  ssnn0fi  12076  fsuppmapnn0fiub  12079  suppssfz  12082  sswrd  12541  sswrdOLD  12542  rtrclreclem3  12975  isercoll  13572  summolem2a  13619  fsumcvg3  13633  fsum2dlem  13667  fsumcom2  13671  qshash  13721  prodmolem2a  13823  fprod2dlem  13866  fprodcom2  13870  bitsfzo  14169  phimullem  14393  prmreclem5  14522  1arith  14529  vdwlem2  14584  vdwlem6  14588  vdwlem8  14590  ramtlecl  14602  monhom  15223  epihom  15230  funcsetcres2  15571  funcestrcsetclem8  15615  funcsetcestrclem8  15630  psdmrn  16036  psssdm2  16044  gsumwspan  16213  frmdss2  16230  ssnmz  16442  conjnmz  16499  gex1  16810  sylow2alem1  16836  sylow3lem3  16848  lsmless1x  16863  lsmless2x  16864  lsmub1x  16865  lsmub2x  16866  lsmmod  16892  lsmdisj2  16899  efgrelexlemb  16967  efgcpbllemb  16972  cntzcmn  17047  gsum2d2  17198  dprdub  17267  dprdss  17271  dprddisj2  17282  dprddisj2OLD  17283  ablfacrp  17312  pgpfac1lem3  17323  kerf1hrm  17587  isdrng2  17601  subrguss  17639  subrgmre  17648  lssssr  17794  lsssssubg  17799  lssmre  17807  lbspss  17923  lspdisj  17966  lbsextlem2  18000  lidl1el  18061  drngnidl  18072  lpiss  18093  unitrrg  18137  fidomndrng  18151  mplbas2  18329  mplbas2OLD  18330  zsssubrg  18671  qsssubdrg  18672  cnsubrg  18673  mulgrhm2  18711  znrrg  18777  ocvocv  18875  ocv2ss  18877  ocvin  18878  lsmcss  18896  cssmre  18897  pjfo  18919  pjcss  18920  obs2ss  18933  frlmsslsp  18998  lindfrn  19023  dmatsgrp  19168  scmatsgrp  19188  scmatsgrp1  19191  m2cpmrngiso  19426  bastg  19634  tgss  19637  tgtop  19642  tgidm  19649  en2top  19654  neisspw  19775  topssnei  19792  neiptopuni  19798  lpss3  19812  clslp  19816  tgrest  19827  ssrest  19844  restfpw  19847  restntr  19850  ordtbas2  19859  ordtbas  19860  cnss1  19944  cnss2  19945  cnsscnp  19947  cnrest2r  19955  cmpsublem  20066  cmpsub  20067  tgcmp  20068  cmpcld  20069  hauscmplem  20073  cnconn  20089  2ndcsep  20126  llyss  20146  nllyss  20147  restnlly  20149  restlly  20150  locfincmp  20193  locfincf  20198  kgenss  20210  kgenidm  20214  llycmpkgen2  20217  1stckgen  20221  kgen2ss  20222  kgencn3  20225  ptbasfi  20248  ptpjopn  20279  ptclsg  20282  txdis  20299  txkgen  20319  xkoptsub  20321  xkopjcn  20323  txcon  20356  qtoptop2  20366  qtopuni  20369  qtopkgen  20377  basqtop  20378  tgqtop  20379  qtopss  20382  qtoprest  20384  qtopomap  20385  qtopcmap  20386  kqsat  20398  kqcldsat  20400  hmphdis  20463  isfild  20525  ssfg  20539  fgss  20540  fgss2  20541  fgfil  20542  fgabs  20546  filcon  20550  fgtr  20557  trfg  20558  uzrest  20564  ufilmax  20574  ufileu  20586  filufint  20587  rnelfm  20620  fmfnfmlem2  20622  fmfnfmlem4  20624  flimss2  20639  flimss1  20640  flimclsi  20645  flimcf  20649  flimsncls  20653  fclssscls  20685  fclsss1  20689  fclsss2  20690  fclscf  20692  uffclsflim  20698  alexsublem  20710  alexsubALTlem3  20715  ptcmplem2  20719  ptcmplem3  20720  cnextf  20732  symgtgp  20766  cldsubg  20775  tsmscl  20799  haustsms2  20801  tgptsmscls  20818  tsmsxp  20823  restutop  20906  restutopopn  20907  ustuqtop4  20913  utop2nei  20919  utop3cls  20920  ucncn  20954  xblss2ps  21070  xblss2  21071  unirnblps  21088  unirnbl  21089  xrsblre  21482  xrsmopn  21483  recld2  21485  zdis  21487  icccmplem2  21494  cncfss  21569  cnheiborlem  21620  htpycn  21639  phtpyhtpy  21648  pi1blem  21705  clsocv  21856  cfilfcls  21879  iscmet3lem2  21897  iscmet2  21899  caussi  21902  equivcfil  21904  lmcau  21917  cmetss  21919  pjth  22020  hlhil  22024  ivthicc  22036  ovoliunnul  22084  ovolicopnf  22101  uniioombllem3  22160  dyadmbllem  22174  opnmbllem  22176  volsup2  22180  vitalilem2  22184  itg1addlem4  22272  itg10a  22283  itg1ge0a  22284  mbfi1fseqlem4  22291  itg2gt0  22333  limciun  22464  perfdvf  22473  dvidlem  22485  cpnord  22504  dvaddf  22511  dvmulf  22512  dvcof  22517  dvcj  22519  dvrec  22524  dvcnv  22544  dvlip2  22562  dvivth  22577  dvne0  22578  dvcnvre  22586  ftc1cn  22610  ply1lpir  22745  plyco0  22755  plyexmo  22875  ulmdv  22964  pserdv  22990  abelth  23002  efif1o  23099  logno1  23185  efopnlem2  23206  loglesqrt  23300  ppisval  23575  ppisval2  23576  ppinprm  23624  chtnprm  23626  fsumvma  23686  dchrfi  23728  chtppilimlem2  23857  chebbnd2  23860  vmadivsumb  23866  rplogsumlem2  23868  dchrisumlem2  23873  vmalogdivsum2  23921  vmalogdivsum  23922  2vmadivsumlem  23923  selbergb  23932  selberg2b  23935  selberg3lem1  23940  selberg3lem2  23941  selberg3  23942  selberg4lem1  23943  selberg4  23944  pntrlog2bndlem2  23961  pntrlog2bndlem4  23963  sizeusglecusglem1  24686  clwwlkssclwwlkn  24994  ococss  26409  shsub1  26440  shless  26475  shmodsi  26505  pjhth  26509  spansnss  26687  spanpr  26696  spansnm0i  26766  pjjsi  26816  sumdmdii  27532  sumdmdlem  27535  sumdmdlem2  27536  cdj3lem1  27551  abrexss  27609  rnmpt2ss  27742  unifi3  27758  ssnnssfz  27831  reff  28077  crefss  28087  cmpcref  28088  tpr2rico  28129  esumrnmpt2  28297  esumpcvgval  28307  sigapildsys  28388  cldssbrsiga  28395  measdivcstOLD  28432  mbfmcnt  28476  dya2iocuni  28491  oddpwdc  28557  eulerpartlemgs2  28583  lgamcvg2  28861  sconpi1  28948  cvmscld  28982  cvmsss2  28983  cvmliftlem15  29007  dfon2lem6  29460  predpo  29504  preddowncl  29516  wfrlem10  29592  nofulllem5  29706  supaddc  30281  supadd  30282  opnmbllem0  30290  ftc1cnnc  30329  fnessref  30415  fgmin  30428  tailfb  30435  sstotbnd3  30512  prdstotbnd  30530  cntotbnd  30532  ismtyhmeo  30541  1idl  30663  eldiophss  30947  rencldnfilem  30993  pellexlem5  31008  pell14qrss1234  31031  pell1qrss14  31043  pellfundre  31056  pellfundge  31057  pellfundlb  31059  pellfundglb  31060  harinf  31215  kercvrlsm  31268  pwssplit4  31274  hbtlem5  31318  proot1hash  31401  radcnvrat  31436  nznngen  31462  refsumcn  31645  icoiccdif  31803  lptioo2  31876  lptioo1  31877  icccncfext  31929  stoweidlem27  32048  stoweidlem46  32067  stoweidlem57  32078  fourierdlem40  32168  fourierdlem78  32206  ffnafv  32495  elpwdifsn  32670  rnghmsscmap2  33035  rnghmsscmap  33036  funcrngcsetc  33060  funcrngcsetcALT  33061  rhmsscmap2  33081  rhmsscmap  33082  rhmsscrnghm  33088  rngcresringcat  33092  funcringcsetc  33097  funcringcsetcALTV2lem8  33105  funcringcsetclem8ALTV  33128  rhmsubcALTVlem4  33170  ssnn0ssfz  33192  lincolss  33289  lcoss  33291  lcosslsp  33293  trsspwALT3  34012  sspwimpALT2  34129  bnj1033  34426  bnj1398  34491  lshpdisj  35109  lssats  35134  lkrlsp  35224  lkrin  35286  glbconxN  35499  paddss1  35938  paddss2  35939  paddasslem16  35956  paddidm  35962  pmodlem2  35968  pmapjoin  35973  pmapjat1  35974  pclfinN  36021  pclfinclN  36071  cdleme50rnlem  36667  diasslssN  37183  dia2dimlem12  37199  dihsslss  37400  baerlem3lem2  37834  baerlem5alem2  37835  baerlem5blem2  37836  hdmaprnN  37991  hgmaprnN  38028  ov2ssiunov2  38201
  Copyright terms: Public domain W3C validator