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

Theorem ssrdv 3493
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 1704 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3476 . 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 1379    e. wcel 1802    C_ wss 3459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3466  df-ss 3473
This theorem is referenced by:  sscon  3621  ssdif  3622  unss1  3656  ssrin  3706  eq0rdv  3803  uniss  4252  intss1  4283  intmin  4288  intssuni  4291  iunss1  4324  iinss1  4325  ss2iun  4328  ssiun  4354  ssiun2  4355  iinss  4363  iinss2  4364  trintss  4543  sspwb  4683  pwssun  4773  tron  4888  tz7.7  4891  xpsspw  5103  relop  5140  dmss  5189  dmcosseq  5251  ssrnres  5432  sossfld  5441  dffv2  5928  chfnrn  5980  suppssOLD  6002  fvn0ssdmfun  6004  fveqdmss  6008  dff3  6026  ffnfv  6039  f1imass  6154  ssorduni  6603  onint  6612  limsssuc  6667  limuni3  6669  limomss  6687  fo1stres  6806  fo2ndres  6807  fo2ndf  6889  fnse  6899  ressuppssdif  6920  suppss  6929  reldmtpos  6962  onfununi  7011  smoiun  7031  smorndom  7038  tz7.48-1  7107  tz7.49  7109  oaass  7209  qsss  7371  uniinqs  7390  pmss12g  7444  mapss  7460  ixpssmap2g  7497  ixpssmapg  7498  fineqv  7734  pssnn  7737  ssfii  7878  dffi2  7882  ordtypelem9  7951  ordtypelem10  7952  oismo  7965  unxpwdom2  8014  inf3lemd  8044  inf3lem1  8045  inf3lem6  8050  cantnflem3  8110  cantnf  8112  cantnflem3OLD  8132  cantnfOLD  8134  cnfcom3lem  8147  cnfcom3lemOLD  8155  onssr1  8249  rankunb  8268  tcrank  8302  harcard  8359  carduni  8362  infxpenlem  8391  infpwfien  8443  dfac12r  8526  ackbij2lem1  8599  ackbij1lem18  8617  isfin1-3  8766  fin1a2lem11  8790  fin1a2lem13  8792  zorn2lem4  8879  zorn2lem5  8880  ttukeylem6  8894  ttukeylem7  8895  fpwwe2lem11  9018  fpwwe2lem12  9019  fpwwe2  9021  wunr1om  9097  wunom  9098  tskr1om  9145  tskr1om2  9146  tskxpss  9150  tskcard  9159  tskuni  9161  grothomex  9207  genpss  9382  distrlem1pr  9403  distrlem5pr  9405  prlem934  9411  ltexprlem2  9415  ltexprlem6  9419  ltexprlem7  9420  reclem3pr  9427  reclem4pr  9428  supmul1  10511  supmullem2  10513  peano5uzi  10954  uzss  11107  ixxdisj  11550  ixxss1  11553  ixxss2  11554  ixxss12  11555  ixxub  11556  ixxlb  11557  iocssre  11610  icossre  11611  iccssre  11612  icodisj  11651  fzss1  11728  fzss2  11729  fzosplit  11834  fzouzsplit  11836  ssfzo12bi  11883  ssnn0fi  12070  fsuppmapnn0fiub  12073  suppssfz  12076  sswrd  12531  isercoll  13466  summolem2a  13513  fsumcvg3  13527  fsum2dlem  13561  fsumcom2  13565  qshash  13615  bitsfzo  13959  phimullem  14183  prmreclem5  14312  1arith  14319  vdwlem2  14374  vdwlem6  14378  vdwlem8  14380  ramtlecl  14392  monhom  15004  epihom  15011  funcsetcres2  15291  psdmrn  15708  psssdm2  15716  gsumwspan  15885  frmdss2  15902  ssnmz  16114  conjnmz  16171  gex1  16482  sylow2alem1  16508  sylow3lem3  16520  lsmless1x  16535  lsmless2x  16536  lsmub1x  16537  lsmub2x  16538  lsmmod  16564  lsmdisj2  16571  efgrelexlemb  16639  efgcpbllemb  16644  cntzcmn  16719  gsum2d2  16873  dprdub  16943  dprdss  16947  dprddisj2  16958  dprddisj2OLD  16959  ablfacrp  16988  pgpfac1lem3  16999  kerf1hrm  17263  isdrng2  17277  subrguss  17315  subrgmre  17324  lssssr  17470  lsssssubg  17475  lssmre  17483  lbspss  17599  lspdisj  17642  lbsextlem2  17676  lidl1el  17737  drngnidl  17748  lpiss  17769  unitrrg  17813  fidomndrng  17827  mplbas2  18005  mplbas2OLD  18006  zsssubrg  18347  qsssubdrg  18348  cnsubrg  18349  mulgrhm2  18403  mulgrhm2OLD  18406  znrrg  18474  ocvocv  18572  ocv2ss  18574  ocvin  18575  lsmcss  18593  cssmre  18594  pjfo  18616  pjcss  18617  obs2ss  18630  frlmsslsp  18699  frlmsslspOLD  18700  lindfrn  18726  dmatsgrp  18871  scmatsgrp  18891  scmatsgrp1  18894  m2cpmrngiso  19129  bastg  19337  tgss  19340  tgtop  19345  tgidm  19352  en2top  19357  neisspw  19478  topssnei  19495  neiptopuni  19501  lpss3  19515  clslp  19519  tgrest  19530  ssrest  19547  restfpw  19550  restntr  19553  ordtbas2  19562  ordtbas  19563  cnss1  19647  cnss2  19648  cnsscnp  19650  cnrest2r  19658  cmpsublem  19769  cmpsub  19770  tgcmp  19771  cmpcld  19772  hauscmplem  19776  cnconn  19793  2ndcsep  19830  llyss  19850  nllyss  19851  restnlly  19853  restlly  19854  locfincmp  19897  locfincf  19902  kgenss  19914  kgenidm  19918  llycmpkgen2  19921  1stckgen  19925  kgen2ss  19926  kgencn3  19929  ptbasfi  19952  ptpjopn  19983  ptclsg  19986  txdis  20003  txkgen  20023  xkoptsub  20025  xkopjcn  20027  txcon  20060  qtoptop2  20070  qtopuni  20073  qtopkgen  20081  basqtop  20082  tgqtop  20083  qtopss  20086  qtoprest  20088  qtopomap  20089  qtopcmap  20090  kqsat  20102  kqcldsat  20104  hmphdis  20167  isfild  20229  ssfg  20243  fgss  20244  fgss2  20245  fgfil  20246  fgabs  20250  filcon  20254  fgtr  20261  trfg  20262  uzrest  20268  ufilmax  20278  ufileu  20290  filufint  20291  rnelfm  20324  fmfnfmlem2  20326  fmfnfmlem4  20328  flimss2  20343  flimss1  20344  flimclsi  20349  flimcf  20353  flimsncls  20357  fclssscls  20389  fclsss1  20393  fclsss2  20394  fclscf  20396  uffclsflim  20402  alexsublem  20414  alexsubALTlem3  20419  ptcmplem2  20423  ptcmplem3  20424  cnextf  20436  symgtgp  20470  cldsubg  20479  tsmscl  20503  haustsms2  20505  tgptsmscls  20522  tsmsxp  20527  restutop  20610  restutopopn  20611  ustuqtop4  20617  utop2nei  20623  utop3cls  20624  ucncn  20658  xblss2ps  20774  xblss2  20775  unirnblps  20792  unirnbl  20793  xrsblre  21186  xrsmopn  21187  recld2  21189  zdis  21191  icccmplem2  21198  cncfss  21273  cnheiborlem  21324  htpycn  21343  phtpyhtpy  21352  pi1blem  21409  clsocv  21560  cfilfcls  21583  iscmet3lem2  21601  iscmet2  21603  caussi  21606  equivcfil  21608  lmcau  21621  cmetss  21623  pjth  21724  hlhil  21728  ivthicc  21740  ovoliunnul  21788  ovolicopnf  21805  uniioombllem3  21864  dyadmbllem  21878  opnmbllem  21880  volsup2  21884  vitalilem2  21888  itg1addlem4  21976  itg10a  21987  itg1ge0a  21988  mbfi1fseqlem4  21995  itg2gt0  22037  limciun  22168  perfdvf  22177  dvidlem  22189  cpnord  22208  dvaddf  22215  dvmulf  22216  dvcof  22221  dvcj  22223  dvrec  22228  dvcnv  22248  dvlip2  22266  dvivth  22281  dvne0  22282  dvcnvre  22290  ftc1cn  22314  ply1lpir  22449  plyco0  22459  plyexmo  22578  ulmdv  22667  pserdv  22693  abelth  22705  efif1o  22802  logno1  22886  efopnlem2  22907  loglesqrt  23001  ppisval  23246  ppisval2  23247  ppinprm  23295  chtnprm  23297  fsumvma  23357  dchrfi  23399  chtppilimlem2  23528  chebbnd2  23531  vmadivsumb  23537  rplogsumlem2  23539  dchrisumlem2  23544  vmalogdivsum2  23592  vmalogdivsum  23593  2vmadivsumlem  23594  selbergb  23603  selberg2b  23606  selberg3lem1  23611  selberg3lem2  23612  selberg3  23613  selberg4lem1  23614  selberg4  23615  pntrlog2bndlem2  23632  pntrlog2bndlem4  23634  sizeusglecusglem1  24353  clwwlkssclwwlkn  24661  ococss  26080  shsub1  26111  shless  26146  shmodsi  26176  pjhth  26180  spansnss  26358  spanpr  26367  spansnm0i  26437  pjjsi  26487  sumdmdii  27203  sumdmdlem  27206  sumdmdlem2  27207  cdj3lem1  27222  abrexss  27279  rnmpt2ss  27384  unifi3  27397  ssnnssfz  27466  reff  27712  crefss  27722  cmpcref  27723  tpr2rico  27764  esumpcvgval  27954  cldssbrsiga  28028  measdivcstOLD  28065  mbfmcnt  28109  dya2iocuni  28124  oddpwdc  28163  eulerpartlemgs2  28189  lgamcvg2  28467  sconpi1  28554  cvmscld  28588  cvmsss2  28589  cvmliftlem15  28613  rtrclreclem.trans  28939  prodmolem2a  29038  fprod2dlem  29082  fprodcom2  29086  dfon2lem6  29192  predpo  29236  preddowncl  29248  wfrlem10  29324  nofulllem5  29438  supaddc  30013  supadd  30014  opnmbllem0  30022  ftc1cnnc  30061  fnessref  30147  fgmin  30160  tailfb  30167  sstotbnd3  30244  prdstotbnd  30262  cntotbnd  30264  ismtyhmeo  30273  1idl  30395  eldiophss  30680  rencldnfilem  30726  pellexlem5  30741  pell14qrss1234  30764  pell1qrss14  30776  pellfundre  30789  pellfundge  30790  pellfundlb  30792  pellfundglb  30793  harinf  30948  kercvrlsm  31001  pwssplit4  31007  hbtlem5  31049  proot1hash  31133  radcnvrat  31168  nznngen  31194  refsumcn  31356  icoiccdif  31500  lptioo2  31545  lptioo1  31546  icccncfext  31597  stoweidlem27  31698  stoweidlem46  31717  stoweidlem57  31728  fourierdlem40  31818  fourierdlem78  31856  ffnafv  32094  elpwdifsn  32134  funcestrcsetclem8  32499  rnghmsscmap2  32518  rnghmsscmap  32519  funcrngcsetc  32542  rhmsscmap2  32559  rhmsscmap  32560  rhmsscrnghm  32566  rngcresringcat  32570  funcringcsetc  32575  funcringcsetcOLD2lem8  32583  funcringcsetclem8OLD  32606  rhmsubcOLDlem4  32644  ssnn0ssfz  32666  lincolss  32765  lcoss  32767  lcosslsp  32769  trsspwALT3  33346  sspwimpALT2  33456  bnj1033  33753  bnj1398  33818  lshpdisj  34435  lssats  34460  lkrlsp  34550  lkrin  34612  glbconxN  34825  paddss1  35264  paddss2  35265  paddasslem16  35282  paddidm  35288  pmodlem2  35294  pmapjoin  35299  pmapjat1  35300  pclfinN  35347  pclfinclN  35397  cdleme50rnlem  35993  diasslssN  36509  dia2dimlem12  36525  dihsslss  36726  baerlem3lem2  37160  baerlem5alem2  37161  baerlem5blem2  37162  hdmaprnN  37317  hgmaprnN  37354
  Copyright terms: Public domain W3C validator