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

Theorem ssrdv 3510
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 1695 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3493 . 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 1377    e. wcel 1767    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  sscon  3638  ssdif  3639  unss1  3673  ssrin  3723  eq0rdv  3820  uniss  4266  intss1  4297  intmin  4302  intssuni  4304  iunss1  4337  iinss1  4338  ss2iun  4341  ssiun  4367  ssiun2  4368  iinss  4376  iinss2  4377  trintss  4556  sspwb  4696  pwssun  4786  tron  4901  tz7.7  4904  xpsspw  5114  relop  5151  dmss  5200  dmcosseq  5262  ssrnres  5443  sossfld  5452  dffv2  5938  chfnrn  5990  suppssOLD  6012  dff3  6032  ffnfv  6045  f1imass  6158  ssorduni  6599  onint  6608  limsssuc  6663  limuni3  6665  limomss  6683  fo1stres  6805  fo2ndres  6806  fo2ndf  6887  fnse  6897  ressuppssdif  6918  suppss  6927  reldmtpos  6960  onfununi  7009  smoiun  7029  smorndom  7036  tz7.48-1  7105  tz7.49  7107  oaass  7207  qsss  7369  uniinqs  7388  pmss12g  7442  mapss  7458  ixpssmap2g  7495  ixpssmapg  7496  fineqv  7732  pssnn  7735  ssfii  7875  dffi2  7879  ordtypelem9  7947  ordtypelem10  7948  oismo  7961  unxpwdom2  8010  inf3lemd  8040  inf3lem1  8041  inf3lem6  8046  cantnflem3  8106  cantnf  8108  cantnflem3OLD  8128  cantnfOLD  8130  cnfcom3lem  8143  cnfcom3lemOLD  8151  onssr1  8245  rankunb  8264  tcrank  8298  harcard  8355  carduni  8358  infxpenlem  8387  infpwfien  8439  dfac12r  8522  ackbij2lem1  8595  ackbij1lem18  8613  isfin1-3  8762  fin1a2lem11  8786  fin1a2lem13  8788  zorn2lem4  8875  zorn2lem5  8876  ttukeylem6  8890  ttukeylem7  8891  fpwwe2lem11  9014  fpwwe2lem12  9015  fpwwe2  9017  wunr1om  9093  wunom  9094  tskr1om  9141  tskr1om2  9142  tskxpss  9146  tskcard  9155  tskuni  9157  grothomex  9203  genpss  9378  distrlem1pr  9399  distrlem5pr  9401  prlem934  9407  ltexprlem2  9411  ltexprlem6  9415  ltexprlem7  9416  reclem3pr  9423  reclem4pr  9424  supmul1  10504  supmullem2  10506  peano5uzi  10945  uzss  11098  ixxdisj  11540  ixxss1  11543  ixxss2  11544  ixxss12  11545  ixxub  11546  ixxlb  11547  iocssre  11600  icossre  11601  iccssre  11602  icodisj  11641  fzss1  11718  fzss2  11719  fzosplit  11822  fzouzsplit  11824  ssfzo12bi  11871  fsuppmapnn0fiub  12061  suppssfz  12064  sswrd  12517  isercoll  13449  summolem2a  13496  fsumcvg3  13510  fsum2dlem  13544  fsumcom2  13548  qshash  13598  bitsfzo  13940  phimullem  14164  prmreclem5  14293  1arith  14300  vdwlem2  14355  vdwlem6  14359  vdwlem8  14361  ramtlecl  14373  monhom  14987  epihom  14994  funcsetcres2  15274  psdmrn  15690  psssdm2  15698  gsumwspan  15837  frmdss2  15854  ssnmz  16038  conjnmz  16095  gex1  16407  sylow2alem1  16433  sylow3lem3  16445  lsmless1x  16460  lsmless2x  16461  lsmub1x  16462  lsmub2x  16463  lsmmod  16489  lsmdisj2  16496  efgrelexlemb  16564  efgcpbllemb  16569  cntzcmn  16641  gsum2d2  16793  dprdub  16862  dprdss  16866  dprddisj2  16877  dprddisj2OLD  16878  ablfacrp  16907  pgpfac1lem3  16918  kerf1hrm  17175  isdrng2  17189  subrguss  17227  subrgmre  17236  lssssr  17382  lsssssubg  17387  lssmre  17395  lbspss  17511  lspdisj  17554  lbsextlem2  17588  lidl1el  17648  drngnidl  17659  lpiss  17680  unitrrg  17713  fidomndrng  17727  mplbas2  17905  mplbas2OLD  17906  zsssubrg  18244  qsssubdrg  18245  cnsubrg  18246  mulgrhm2  18300  mulgrhm2OLD  18303  znrrg  18371  ocvocv  18469  ocv2ss  18471  ocvin  18472  lsmcss  18490  cssmre  18491  pjfo  18513  pjcss  18514  obs2ss  18527  frlmsslsp  18596  frlmsslspOLD  18597  lindfrn  18623  dmatsgrp  18768  scmatsgrp  18788  scmatsgrp1  18791  m2cpmrngiso  19026  bastg  19234  tgss  19236  tgtop  19241  tgidm  19248  en2top  19253  neisspw  19374  topssnei  19391  neiptopuni  19397  lpss3  19411  clslp  19415  tgrest  19426  ssrest  19443  restfpw  19446  restntr  19449  ordtbas2  19458  ordtbas  19459  cnss1  19543  cnss2  19544  cnsscnp  19546  cnrest2r  19554  cmpsublem  19665  cmpsub  19666  tgcmp  19667  cmpcld  19668  hauscmplem  19672  cnconn  19689  2ndcsep  19726  llyss  19746  nllyss  19747  restnlly  19749  restlly  19750  kgenss  19779  kgenidm  19783  llycmpkgen2  19786  1stckgen  19790  kgen2ss  19791  kgencn3  19794  ptbasfi  19817  ptpjopn  19848  ptclsg  19851  txdis  19868  txkgen  19888  xkoptsub  19890  xkopjcn  19892  txcon  19925  qtoptop2  19935  qtopuni  19938  qtopkgen  19946  basqtop  19947  tgqtop  19948  qtopss  19951  qtoprest  19953  qtopomap  19954  qtopcmap  19955  kqsat  19967  kqcldsat  19969  hmphdis  20032  isfild  20094  ssfg  20108  fgss  20109  fgss2  20110  fgfil  20111  fgabs  20115  filcon  20119  fgtr  20126  trfg  20127  uzrest  20133  ufilmax  20143  ufileu  20155  filufint  20156  rnelfm  20189  fmfnfmlem2  20191  fmfnfmlem4  20193  flimss2  20208  flimss1  20209  flimclsi  20214  flimcf  20218  flimsncls  20222  fclssscls  20254  fclsss1  20258  fclsss2  20259  fclscf  20261  uffclsflim  20267  alexsublem  20279  alexsubALTlem3  20284  ptcmplem2  20288  ptcmplem3  20289  cnextf  20301  symgtgp  20335  cldsubg  20344  tsmscl  20368  haustsms2  20370  tgptsmscls  20387  tsmsxp  20392  restutop  20475  restutopopn  20476  ustuqtop4  20482  utop2nei  20488  utop3cls  20489  ucncn  20523  xblss2ps  20639  xblss2  20640  unirnblps  20657  unirnbl  20658  xrsblre  21051  xrsmopn  21052  recld2  21054  zdis  21056  icccmplem2  21063  cncfss  21138  cnheiborlem  21189  htpycn  21208  phtpyhtpy  21217  pi1blem  21274  clsocv  21425  cfilfcls  21448  iscmet3lem2  21466  iscmet2  21468  caussi  21471  equivcfil  21473  lmcau  21486  cmetss  21488  pjth  21589  hlhil  21593  ivthicc  21605  ovoliunnul  21653  ovolicopnf  21670  uniioombllem3  21729  dyadmbllem  21743  opnmbllem  21745  volsup2  21749  vitalilem2  21753  itg1addlem4  21841  itg10a  21852  itg1ge0a  21853  mbfi1fseqlem4  21860  itg2gt0  21902  limciun  22033  perfdvf  22042  dvidlem  22054  cpnord  22073  dvaddf  22080  dvmulf  22081  dvcof  22086  dvcj  22088  dvrec  22093  dvcnv  22113  dvlip2  22131  dvivth  22146  dvne0  22147  dvcnvre  22155  ftc1cn  22179  ply1lpir  22314  plyco0  22324  plyexmo  22443  ulmdv  22532  pserdv  22558  abelth  22570  efif1o  22666  logno1  22745  efopnlem2  22766  loglesqrt  22860  ppisval  23105  ppisval2  23106  ppinprm  23154  chtnprm  23156  fsumvma  23216  dchrfi  23258  chtppilimlem2  23387  chebbnd2  23390  vmadivsumb  23396  rplogsumlem2  23398  dchrisumlem2  23403  vmalogdivsum2  23451  vmalogdivsum  23452  2vmadivsumlem  23453  selbergb  23462  selberg2b  23465  selberg3lem1  23470  selberg3lem2  23471  selberg3  23472  selberg4lem1  23473  selberg4  23474  pntrlog2bndlem2  23491  pntrlog2bndlem4  23493  sizeusglecusglem1  24160  ococss  25887  shsub1  25918  shless  25953  shmodsi  25983  pjhth  25987  spansnss  26165  spanpr  26174  spansnm0i  26244  pjjsi  26294  sumdmdii  27010  sumdmdlem  27013  sumdmdlem2  27014  cdj3lem1  27029  abrexss  27084  rnmpt2ss  27187  unifi3  27200  ssnnssfz  27265  tpr2rico  27530  esumpcvgval  27724  cldssbrsiga  27798  measdivcstOLD  27835  mbfmcnt  27879  dya2iocuni  27894  oddpwdc  27933  eulerpartlemgs2  27959  lgamcvg2  28237  sconpi1  28324  cvmscld  28358  cvmsss2  28359  cvmliftlem15  28383  rtrclreclem.trans  28544  prodmolem2a  28643  fprod2dlem  28687  fprodcom2  28691  dfon2lem6  28797  predpo  28841  preddowncl  28853  wfrlem10  28929  nofulllem5  29043  supaddc  29618  supadd  29619  opnmbllem0  29627  ftc1cnnc  29666  fnessref  29765  locfincmp  29776  locfincf  29778  fgmin  29791  tailfb  29798  sstotbnd3  29875  prdstotbnd  29893  cntotbnd  29895  ismtyhmeo  29904  1idl  30026  eldiophss  30312  rencldnfilem  30358  pellexlem5  30373  pell14qrss1234  30396  pell1qrss14  30408  pellfundre  30421  pellfundge  30422  pellfundlb  30424  pellfundglb  30425  harinf  30580  kercvrlsm  30633  pwssplit4  30639  hbtlem5  30681  proot1hash  30765  nznngen  30821  refsumcn  30983  lptioo2  31173  lptioo1  31174  stoweidlem27  31327  stoweidlem46  31346  stoweidlem57  31357  fourierdlem40  31447  fourierdlem78  31485  ffnafv  31723  elpwdifsn  31763  ssnn0ssfz  32002  lincolss  32108  lcoss  32110  lcosslsp  32112  trsspwALT3  32698  sspwimpALT2  32808  bnj1033  33104  bnj1398  33169  lshpdisj  33784  lssats  33809  lkrlsp  33899  lkrin  33961  glbconxN  34174  paddss1  34613  paddss2  34614  paddasslem16  34631  paddidm  34637  pmodlem2  34643  pmapjoin  34648  pmapjat1  34649  pclfinN  34696  pclfinclN  34746  cdleme50rnlem  35340  diasslssN  35856  dia2dimlem12  35872  dihsslss  36073  baerlem3lem2  36507  baerlem5alem2  36508  baerlem5blem2  36509  hdmaprnN  36664  hgmaprnN  36701
  Copyright terms: Public domain W3C validator