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

Theorem ssrdv 3350
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 1684 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3333 . 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 1360    e. wcel 1755    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  sscon  3478  ssdif  3479  unss1  3513  ssrin  3563  eq0rdv  3660  uniss  4100  intss1  4131  intmin  4136  intssuni  4138  iunss1  4170  iinss1  4171  ss2iun  4174  ssiun  4200  ssiun2  4201  iinss  4209  iinss2  4210  trintss  4389  sspwb  4529  pwssun  4614  tron  4729  tz7.7  4732  xpsspw  4940  relop  4977  dmss  5026  dmcosseq  5088  ssrnres  5264  sossfld  5273  dffv2  5752  chfnrn  5802  suppssOLD  5824  dff3  5844  ffnfv  5856  f1imass  5964  ssorduni  6386  onint  6395  limsssuc  6450  limuni3  6452  limomss  6470  fo1stres  6589  fo2ndres  6590  fo2ndf  6668  fnse  6678  ressuppssdif  6699  suppss  6708  reldmtpos  6742  onfununi  6788  smoiun  6808  smorndom  6815  tz7.48-1  6884  tz7.49  6886  oaass  6988  qsss  7149  uniinqs  7168  pmss12g  7227  mapss  7243  ixpssmap2g  7280  ixpssmapg  7281  fineqv  7516  pssnn  7519  ssfii  7657  dffi2  7661  ordtypelem9  7728  ordtypelem10  7729  oismo  7742  unxpwdom2  7791  inf3lemd  7821  inf3lem1  7822  inf3lem6  7827  cantnflem3  7887  cantnf  7889  cantnflem3OLD  7909  cantnfOLD  7911  cnfcom3lem  7924  cnfcom3lemOLD  7932  onssr1  8026  rankunb  8045  tcrank  8079  harcard  8136  carduni  8139  infxpenlem  8168  infpwfien  8220  dfac12r  8303  ackbij2lem1  8376  ackbij1lem18  8394  isfin1-3  8543  fin1a2lem11  8567  fin1a2lem13  8569  zorn2lem4  8656  zorn2lem5  8657  ttukeylem6  8671  ttukeylem7  8672  fpwwe2lem11  8794  fpwwe2lem12  8795  fpwwe2  8797  wunr1om  8873  wunom  8874  tskr1om  8921  tskr1om2  8922  tskxpss  8926  tskcard  8935  tskuni  8937  grothomex  8983  genpss  9160  distrlem1pr  9181  distrlem5pr  9183  prlem934  9189  ltexprlem2  9193  ltexprlem6  9197  ltexprlem7  9198  reclem3pr  9205  reclem4pr  9206  supmul1  10282  supmullem2  10284  peano5uzi  10717  uzss  10868  ixxdisj  11302  ixxss1  11305  ixxss2  11306  ixxss12  11307  ixxub  11308  ixxlb  11309  iocssre  11362  icossre  11363  iccssre  11364  icodisj  11396  fzss1  11483  fzss2  11484  fzosplit  11565  fzouzsplit  11567  ssfzo12bi  11605  sswrd  12225  isercoll  13128  summolem2a  13175  fsumcvg3  13189  fsum2dlem  13220  fsumcom2  13224  qshash  13272  bitsfzo  13613  phimullem  13836  prmreclem5  13963  1arith  13970  vdwlem2  14025  vdwlem6  14029  vdwlem8  14031  ramtlecl  14043  monhom  14656  epihom  14663  funcsetcres2  14943  psdmrn  15359  psssdm2  15367  gsumwspan  15503  frmdss2  15520  ssnmz  15702  conjnmz  15759  gex1  16069  sylow2alem1  16095  sylow3lem3  16107  lsmless1x  16122  lsmless2x  16123  lsmub1x  16124  lsmub2x  16125  lsmmod  16151  lsmdisj2  16158  efgrelexlemb  16226  efgcpbllemb  16231  cntzcmn  16303  gsum2d2  16439  dprdub  16495  dprdss  16499  dprddisj2  16510  dprddisj2OLD  16511  ablfacrp  16540  pgpfac1lem3  16551  isdrng2  16765  subrguss  16803  subrgmre  16812  lssssr  16955  lsssssubg  16960  lssmre  16968  lbspss  17084  lspdisj  17127  lbsextlem2  17161  lidl1el  17221  drngnidl  17232  lpiss  17253  unitrrg  17286  fidomndrng  17300  mplbas2  17482  mplbas2OLD  17483  zsssubrg  17714  qsssubdrg  17715  cnsubrg  17716  mulgrhm2  17768  mulgrhm2OLD  17771  znrrg  17839  ocvocv  17937  ocv2ss  17939  ocvin  17940  lsmcss  17958  cssmre  17959  pjfo  17981  pjcss  17982  obs2ss  17995  frlmsslsp  18064  frlmsslspOLD  18065  lindfrn  18091  bastg  18412  tgss  18414  tgtop  18419  tgidm  18426  en2top  18431  neisspw  18552  topssnei  18569  neiptopuni  18575  lpss3  18589  clslp  18593  tgrest  18604  ssrest  18621  restfpw  18624  restntr  18627  ordtbas2  18636  ordtbas  18637  cnss1  18721  cnss2  18722  cnsscnp  18724  cnrest2r  18732  cmpsublem  18843  cmpsub  18844  tgcmp  18845  cmpcld  18846  hauscmplem  18850  cnconn  18867  2ndcsep  18904  llyss  18924  nllyss  18925  restnlly  18927  restlly  18928  kgenss  18957  kgenidm  18961  llycmpkgen2  18964  1stckgen  18968  kgen2ss  18969  kgencn3  18972  ptbasfi  18995  ptpjopn  19026  ptclsg  19029  txdis  19046  txkgen  19066  xkoptsub  19068  xkopjcn  19070  txcon  19103  qtoptop2  19113  qtopuni  19116  qtopkgen  19124  basqtop  19125  tgqtop  19126  qtopss  19129  qtoprest  19131  qtopomap  19132  qtopcmap  19133  kqsat  19145  kqcldsat  19147  hmphdis  19210  isfild  19272  ssfg  19286  fgss  19287  fgss2  19288  fgfil  19289  fgabs  19293  filcon  19297  fgtr  19304  trfg  19305  uzrest  19311  ufilmax  19321  ufileu  19333  filufint  19334  rnelfm  19367  fmfnfmlem2  19369  fmfnfmlem4  19371  flimss2  19386  flimss1  19387  flimclsi  19392  flimcf  19396  flimsncls  19400  fclssscls  19432  fclsss1  19436  fclsss2  19437  fclscf  19439  uffclsflim  19445  alexsublem  19457  alexsubALTlem3  19462  ptcmplem2  19466  ptcmplem3  19467  cnextf  19479  symgtgp  19513  cldsubg  19522  tsmscl  19546  haustsms2  19548  tgptsmscls  19565  tsmsxp  19570  restutop  19653  restutopopn  19654  ustuqtop4  19660  utop2nei  19666  utop3cls  19667  ucncn  19701  xblss2ps  19817  xblss2  19818  unirnblps  19835  unirnbl  19836  xrsblre  20229  xrsmopn  20230  recld2  20232  zdis  20234  icccmplem2  20241  cncfss  20316  cnheiborlem  20367  htpycn  20386  phtpyhtpy  20395  pi1blem  20452  clsocv  20603  cfilfcls  20626  iscmet3lem2  20644  iscmet2  20646  caussi  20649  equivcfil  20651  lmcau  20664  cmetss  20666  pjth  20767  hlhil  20771  ivthicc  20783  ovoliunnul  20831  ovolicopnf  20848  uniioombllem3  20906  dyadmbllem  20920  opnmbllem  20922  volsup2  20926  vitalilem2  20930  itg1addlem4  21018  itg10a  21029  itg1ge0a  21030  mbfi1fseqlem4  21037  itg2gt0  21079  limciun  21210  perfdvf  21219  dvidlem  21231  cpnord  21250  dvaddf  21257  dvmulf  21258  dvcof  21263  dvcj  21265  dvrec  21270  dvcnv  21290  dvlip2  21308  dvivth  21323  dvne0  21324  dvcnvre  21332  ftc1cn  21356  ply1lpir  21534  plyco0  21544  plyexmo  21663  ulmdv  21752  pserdv  21778  abelth  21790  efif1o  21886  logno1  21965  efopnlem2  21986  loglesqr  22080  ppisval  22325  ppisval2  22326  ppinprm  22374  chtnprm  22376  fsumvma  22436  dchrfi  22478  chtppilimlem2  22607  chebbnd2  22610  vmadivsumb  22616  rplogsumlem2  22618  dchrisumlem2  22623  vmalogdivsum2  22671  vmalogdivsum  22672  2vmadivsumlem  22673  selbergb  22682  selberg2b  22685  selberg3lem1  22690  selberg3lem2  22691  selberg3  22692  selberg4lem1  22693  selberg4  22694  pntrlog2bndlem2  22711  pntrlog2bndlem4  22713  sizeusglecusglem1  23214  ococss  24518  shsub1  24549  shless  24584  shmodsi  24614  pjhth  24618  spansnss  24796  spanpr  24805  spansnm0i  24875  pjjsi  24925  sumdmdii  25641  sumdmdlem  25644  sumdmdlem2  25645  cdj3lem1  25660  abrexss  25716  rnmpt2ss  25815  unifi3  25828  ssnnssfz  25898  kerf1hrm  26144  tpr2rico  26195  esumpcvgval  26380  cldssbrsiga  26454  measdivcstOLD  26491  mbfmcnt  26536  dya2iocuni  26551  oddpwdc  26584  eulerpartlemgs2  26610  lgamcvg2  26888  sconpi1  26975  cvmscld  27009  cvmsss2  27010  cvmliftlem15  27034  rtrclreclem.trans  27194  prodmolem2a  27293  fprod2dlem  27337  fprodcom2  27341  dfon2lem6  27447  predpo  27491  preddowncl  27503  wfrlem10  27579  nofulllem5  27693  supaddc  28258  supadd  28259  opnmbllem0  28268  ftc1cnnc  28307  fnessref  28406  locfincmp  28417  locfincf  28419  fgmin  28432  tailfb  28439  sstotbnd3  28516  prdstotbnd  28534  cntotbnd  28536  ismtyhmeo  28545  1idl  28667  eldiophss  28955  rencldnfilem  29001  pellexlem5  29016  pell14qrss1234  29039  pell1qrss14  29051  pellfundre  29064  pellfundge  29065  pellfundlb  29067  pellfundglb  29068  harinf  29225  kercvrlsm  29278  pwssplit4  29284  hbtlem5  29326  proot1hash  29410  refsumcn  29594  stoweidlem27  29665  stoweidlem46  29684  stoweidlem57  29695  ffnafv  29920  lincolss  30674  lcoss  30676  lcosslsp  30678  trsspwALT3  31253  sspwimpALT2  31363  bnj1033  31659  bnj1398  31724  lshpdisj  32202  lssats  32227  lkrlsp  32317  lkrin  32379  glbconxN  32592  paddss1  33031  paddss2  33032  paddasslem16  33049  paddidm  33055  pmodlem2  33061  pmapjoin  33066  pmapjat1  33067  pclfinN  33114  pclfinclN  33164  cdleme50rnlem  33758  diasslssN  34274  dia2dimlem12  34290  dihsslss  34491  baerlem3lem2  34925  baerlem5alem2  34926  baerlem5blem2  34927  hdmaprnN  35082  hgmaprnN  35119
  Copyright terms: Public domain W3C validator