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

Theorem ssrdv 3467
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 1763 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3450 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
42, 3sylibr 215 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1435    e. wcel 1867    C_ wss 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-in 3440  df-ss 3447
This theorem is referenced by:  sscon  3596  ssdif  3597  unss1  3632  ssrin  3684  eq0rdv  3794  uniss  4234  intss1  4264  intmin  4269  intssuni  4272  iunss1  4305  iinss1  4306  ss2iun  4309  ssiun  4335  ssiun2  4336  iinss  4344  iinss2  4345  trintss  4527  sspwb  4662  pwssun  4751  relop  4996  dmss  5045  dmcosseq  5107  ssrnres  5286  sossfld  5294  predpo  5408  preddowncl  5417  tron  5456  tz7.7  5459  dffv2  5945  chfnrn  5999  fvn0ssdmfun  6019  fveqdmss  6023  dff3  6041  ffnfv  6055  f1imass  6171  ssorduni  6617  onint  6627  limsssuc  6682  limuni3  6684  limomss  6702  fo1stres  6822  fo2ndres  6823  fo2ndf  6905  fnse  6915  ressuppssdif  6938  suppss  6947  reldmtpos  6980  wfrlem10  7044  onfununi  7059  smoiun  7079  smorndom  7086  tz7.48-1  7159  tz7.49  7161  oaass  7261  qsss  7423  uniinqs  7442  pmss12g  7497  mapss  7513  ixpssmap2g  7550  ixpssmapg  7551  fineqv  7784  pssnn  7787  ssfii  7930  dffi2  7934  ordtypelem9  8032  ordtypelem10  8033  oismo  8046  unxpwdom2  8094  inf3lemd  8123  inf3lem1  8124  inf3lem6  8129  cantnflem3  8186  cantnf  8188  cnfcom3lem  8198  onssr1  8292  rankunb  8311  tcrank  8345  harcard  8402  carduni  8405  infxpenlem  8434  infpwfien  8482  dfac12r  8565  ackbij2lem1  8638  ackbij1lem18  8656  isfin1-3  8805  fin1a2lem11  8829  fin1a2lem13  8831  zorn2lem4  8918  zorn2lem5  8919  ttukeylem6  8933  ttukeylem7  8934  fpwwe2lem11  9054  fpwwe2lem12  9055  fpwwe2  9057  wunr1om  9133  wunom  9134  tskr1om  9181  tskr1om2  9182  tskxpss  9186  tskcard  9195  tskuni  9197  grothomex  9243  genpss  9418  distrlem1pr  9439  distrlem5pr  9441  prlem934  9447  ltexprlem2  9451  ltexprlem6  9455  ltexprlem7  9456  reclem3pr  9463  reclem4pr  9464  supaddc  10563  supadd  10564  supmul1  10565  supmullem2  10567  peano5uzi  11013  uzss  11168  ixxdisj  11639  ixxss1  11642  ixxss2  11643  ixxss12  11644  ixxub  11645  ixxlb  11646  ixxlbOLD  11647  iocssre  11703  icossre  11704  iccssre  11705  icodisj  11744  fzss1  11824  fzss2  11825  fzosplit  11938  fzouzsplit  11940  ssfzo12bi  11992  ssnn0fi  12183  fsuppmapnn0fiub  12189  suppssfz  12192  sswrd  12655  sswrdOLD  12656  rtrclreclem3  13091  isercoll  13698  summolem2a  13748  fsumcvg3  13762  fsum2dlem  13798  fsumcom2  13802  qshash  13852  prodmolem2a  13955  fprod2dlem  14001  fprodcom2  14005  bitsfzo  14372  phimullem  14685  prmreclem5  14816  1arith  14823  vdwlem2  14884  vdwlem6  14888  vdwlem8  14890  ramtlecl  14903  prmgaplem3  14975  prmgaplem4  14976  monhom  15584  epihom  15591  funcsetcres2  15932  funcestrcsetclem8  15976  funcsetcestrclem8  15991  psdmrn  16397  psssdm2  16405  gsumwspan  16574  frmdss2  16591  ssnmz  16803  conjnmz  16860  gex1  17171  sylow2alem1  17197  sylow3lem3  17209  lsmless1x  17224  lsmless2x  17225  lsmub1x  17226  lsmub2x  17227  lsmmod  17253  lsmdisj2  17260  efgrelexlemb  17328  efgcpbllemb  17333  cntzcmn  17408  gsum2d2  17534  dprdub  17586  dprdss  17590  dprddisj2  17600  ablfacrp  17627  pgpfac1lem3  17638  kerf1hrm  17899  isdrng2  17913  subrguss  17951  subrgmre  17960  lssssr  18104  lsssssubg  18109  lssmre  18117  lbspss  18233  lspdisj  18276  lbsextlem2  18310  lidl1el  18370  drngnidl  18381  lpiss  18402  unitrrg  18445  fidomndrng  18459  mplbas2  18622  zsssubrg  18954  qsssubdrg  18955  cnsubrg  18956  mulgrhm2  18994  znrrg  19060  ocvocv  19158  ocv2ss  19160  ocvin  19161  lsmcss  19179  cssmre  19180  pjfo  19202  pjcss  19203  obs2ss  19216  frlmsslsp  19278  lindfrn  19303  dmatsgrp  19448  scmatsgrp  19468  scmatsgrp1  19471  m2cpmrngiso  19706  bastg  19905  tgss  19908  tgtop  19913  tgidm  19920  en2top  19925  neisspw  20047  topssnei  20064  neiptopuni  20070  lpss3  20084  clslp  20088  tgrest  20099  ssrest  20116  restfpw  20119  restntr  20122  ordtbas2  20131  ordtbas  20132  cnss1  20216  cnss2  20217  cnsscnp  20219  cnrest2r  20227  cmpsublem  20338  cmpsub  20339  tgcmp  20340  cmpcld  20341  hauscmplem  20345  cnconn  20361  2ndcsep  20398  llyss  20418  nllyss  20419  restnlly  20421  restlly  20422  locfincmp  20465  locfincf  20470  kgenss  20482  kgenidm  20486  llycmpkgen2  20489  1stckgen  20493  kgen2ss  20494  kgencn3  20497  ptbasfi  20520  ptpjopn  20551  ptclsg  20554  txdis  20571  txkgen  20591  xkoptsub  20593  xkopjcn  20595  txcon  20628  qtoptop2  20638  qtopuni  20641  qtopkgen  20649  basqtop  20650  tgqtop  20651  qtopss  20654  qtoprest  20656  qtopomap  20657  qtopcmap  20658  kqsat  20670  kqcldsat  20672  hmphdis  20735  isfild  20797  ssfg  20811  fgss  20812  fgss2  20813  fgfil  20814  fgabs  20818  filcon  20822  fgtr  20829  trfg  20830  uzrest  20836  ufilmax  20846  ufileu  20858  filufint  20859  rnelfm  20892  fmfnfmlem2  20894  fmfnfmlem4  20896  flimss2  20911  flimss1  20912  flimclsi  20917  flimcf  20921  flimsncls  20925  fclssscls  20957  fclsss1  20961  fclsss2  20962  fclscf  20964  uffclsflim  20970  alexsublem  20983  alexsubALTlem3  20988  ptcmplem2  20992  ptcmplem3  20993  cnextf  21005  symgtgp  21040  cldsubg  21049  tsmscl  21073  haustsms2  21075  tgptsmscls  21088  tsmsxp  21093  restutop  21176  restutopopn  21177  ustuqtop4  21183  utop2nei  21189  utop3cls  21190  ucncn  21224  xblss2ps  21340  xblss2  21341  unirnblps  21358  unirnbl  21359  xrsblre  21733  xrsmopn  21734  recld2  21736  zdis  21738  icccmplem2  21745  cncfss  21820  cnheiborlem  21871  htpycn  21890  phtpyhtpy  21899  pi1blem  21956  clsocv  22107  cfilfcls  22130  iscmet3lem2  22148  iscmet2  22150  caussi  22153  equivcfil  22155  lmcau  22168  cmetss  22170  pjth  22267  hlhil  22271  ivthicc  22283  ovoliunnul  22334  ovolicopnf  22352  uniioombllem3  22417  dyadmbllem  22431  opnmbllem  22433  volsup2  22437  vitalilem2  22441  itg1addlem4  22531  itg10a  22542  itg1ge0a  22543  mbfi1fseqlem4  22550  itg2gt0  22592  limciun  22723  perfdvf  22732  dvidlem  22744  cpnord  22763  dvaddf  22770  dvmulf  22771  dvcof  22776  dvcj  22778  dvrec  22783  dvcnv  22803  dvlip2  22821  dvivth  22836  dvne0  22837  dvcnvre  22845  ftc1cn  22869  ply1lpir  23001  plyco0  23011  plyexmo  23131  ulmdv  23220  pserdv  23246  abelth  23258  efif1o  23357  logno1  23443  efopnlem2  23464  loglesqrt  23560  lgamcvg2  23842  ppisval  23890  ppisval2  23891  ppinprm  23939  chtnprm  23941  fsumvma  24001  dchrfi  24043  chtppilimlem2  24172  chebbnd2  24175  vmadivsumb  24181  rplogsumlem2  24183  dchrisumlem2  24188  vmalogdivsum2  24236  vmalogdivsum  24237  2vmadivsumlem  24238  selbergb  24247  selberg2b  24250  selberg3lem1  24255  selberg3lem2  24256  selberg3  24257  selberg4lem1  24258  selberg4  24259  pntrlog2bndlem2  24276  pntrlog2bndlem4  24278  sizeusglecusglem1  25054  clwwlkssclwwlkn  25362  ococss  26778  shsub1  26809  shless  26844  shmodsi  26874  pjhth  26878  spansnss  27056  spanpr  27065  spansnm0i  27135  pjjsi  27185  sumdmdii  27900  sumdmdlem  27903  sumdmdlem2  27904  cdj3lem1  27919  abrexss  27979  rnmpt2ss  28113  unifi3  28129  ssnnssfz  28200  reff  28502  crefss  28512  cmpcref  28513  tpr2rico  28554  esumrnmpt2  28725  esumpcvgval  28735  ldsysgenld  28818  sigapildsys  28820  ldgenpisys  28824  cldssbrsiga  28845  measdivcstOLD  28882  mbfmcnt  28926  dya2iocuni  28941  oddpwdc  29010  eulerpartlemgs2  29036  bnj1033  29563  bnj1398  29628  sconpi1  29747  cvmscld  29781  cvmsss2  29782  cvmliftlem15  29806  dfon2lem6  30218  nofulllem5  30377  fnessref  30795  fgmin  30808  tailfb  30815  dissneqlem  31473  icoreresf  31486  poimirlem11  31655  poimirlem12  31656  opnmbllem0  31680  ftc1cnnc  31720  sstotbnd3  31812  prdstotbnd  31830  cntotbnd  31832  ismtyhmeo  31841  1idl  31963  lshpdisj  32262  lssats  32287  lkrlsp  32377  lkrin  32439  glbconxN  32652  paddss1  33091  paddss2  33092  paddasslem16  33109  paddidm  33115  pmodlem2  33121  pmapjoin  33126  pmapjat1  33127  pclfinN  33174  pclfinclN  33224  cdleme50rnlem  33820  diasslssN  34336  dia2dimlem12  34352  dihsslss  34553  baerlem3lem2  34987  baerlem5alem2  34988  baerlem5blem2  34989  hdmaprnN  35144  hgmaprnN  35181  eldiophss  35326  rencldnfilem  35372  pellexlem5  35387  pell14qrss1234  35412  pell1qrss14  35424  pellfundre  35439  pellfundge  35440  pellfundlb  35442  pellfundglb  35443  harinf  35599  kercvrlsm  35651  pwssplit4  35657  hbtlem5  35697  proot1hash  35780  ss2iundf  35894  ov2ssiunov2  35935  radcnvrat  36304  nznngen  36306  trsspwALT3  36852  sspwimpALT2  36969  refsumcn  36995  icoiccdif  37214  lptioo2  37287  lptioo1  37288  icccncfext  37341  stoweidlem27  37460  stoweidlem46  37480  stoweidlem57  37491  fourierdlem40  37582  fourierdlem78  37620  ffnafv  38076  iccpartrn  38147  elpwdifsn  38386  rnghmsscmap2  38746  rnghmsscmap  38747  funcrngcsetc  38771  funcrngcsetcALT  38772  rhmsscmap2  38792  rhmsscmap  38793  rhmsscrnghm  38799  rngcresringcat  38803  funcringcsetc  38808  funcringcsetcALTV2lem8  38816  funcringcsetclem8ALTV  38839  rhmsubcALTVlem4  38881  ssnn0ssfz  38903  lincolss  39000  lcoss  39002  lcosslsp  39004
  Copyright terms: Public domain W3C validator