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

Theorem ssrdv 3346
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 1641 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3329 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
42, 3sylibr 204 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549    e. wcel 1725    C_ wss 3312
This theorem is referenced by:  sscon  3473  ssdif  3474  unss1  3508  ssrin  3558  eq0rdv  3654  uniss  4028  intss1  4057  intmin  4062  intssuni  4064  iunss1  4096  iinss1  4097  ss2iun  4100  ssiun  4125  ssiun2  4126  iinss  4134  iinss2  4135  trintss  4310  sspwb  4405  pwssun  4481  tron  4596  tz7.7  4599  ssorduni  4757  onint  4766  limsssuc  4821  limuni3  4823  limomss  4841  xpsspw  4977  relop  5014  dmss  5060  dmcosseq  5128  ssrnres  5300  sossfld  5308  dffv2  5787  chfnrn  5832  suppss  5854  dff3  5873  ffnfv  5885  f1imass  6001  fo1stres  6361  fo2ndres  6362  fo2ndf  6444  fnse  6454  reldmtpos  6478  onfununi  6594  smoiun  6614  smorndom  6621  tz7.48-1  6691  tz7.49  6693  oaass  6795  qsss  6956  uniinqs  6975  pmss12g  7031  mapss  7047  ixpssmap2g  7082  ixpssmapg  7083  fineqv  7315  pssnn  7318  ssfii  7415  dffi2  7419  ordtypelem9  7484  ordtypelem10  7485  oismo  7498  unxpwdom2  7545  inf3lemd  7571  inf3lem1  7572  inf3lem6  7577  cantnflem3  7636  cantnf  7638  cnfcom3lem  7649  onssr1  7746  rankunb  7765  tcrank  7797  harcard  7854  carduni  7857  infxpenlem  7884  infpwfien  7932  dfac12r  8015  ackbij2lem1  8088  ackbij1lem18  8106  isfin1-3  8255  fin1a2lem11  8279  fin1a2lem13  8281  zorn2lem4  8368  zorn2lem5  8369  ttukeylem6  8383  ttukeylem7  8384  fpwwe2lem11  8504  fpwwe2lem12  8505  fpwwe2  8507  wunr1om  8583  wunom  8584  tskr1om  8631  tskr1om2  8632  tskxpss  8636  tskcard  8645  tskuni  8647  grothomex  8693  genpss  8870  distrlem1pr  8891  distrlem5pr  8893  prlem934  8899  ltexprlem2  8903  ltexprlem6  8907  ltexprlem7  8908  reclem3pr  8915  reclem4pr  8916  supmul1  9962  supmullem2  9964  peano5uzi  10347  uzss  10495  ixxdisj  10920  ixxss1  10923  ixxss2  10924  ixxss12  10925  ixxub  10926  ixxlb  10927  iocssre  10979  icossre  10980  iccssre  10981  icodisj  11011  fzss1  11080  fzss2  11081  fzosplit  11154  fzouzsplit  11156  sswrd  11725  isercoll  12449  summolem2a  12497  fsumcvg3  12511  fsum2dlem  12542  fsumcom2  12546  qshash  12594  bitsfzo  12935  phimullem  13156  prmreclem5  13276  1arith  13283  vdwlem2  13338  vdwlem6  13342  vdwlem8  13344  ramtlecl  13356  monhom  13949  epihom  13956  funcsetcres2  14236  psdmrn  14627  psssdm2  14635  gsumwspan  14779  frmdss2  14796  ssnmz  14970  conjnmz  15027  gex1  15213  sylow2alem1  15239  sylow3lem3  15251  lsmless1x  15266  lsmless2x  15267  lsmub1x  15268  lsmub2x  15269  lsmmod  15295  lsmdisj2  15302  efgrelexlemb  15370  efgcpbllemb  15375  cntzcmn  15447  gsum2d2  15536  dprdub  15571  dprdss  15575  dprddisj2  15585  ablfacrp  15612  pgpfac1lem3  15623  isdrng2  15833  subrguss  15871  subrgmre  15880  lssssr  16017  lsssssubg  16022  lssmre  16030  lbspss  16142  lspdisj  16185  lbsextlem2  16219  lidl1el  16277  drngnidl  16288  lpiss  16309  unitrrg  16341  fidomndrng  16355  mplbas2  16519  zsssubrg  16745  qsssubdrg  16746  cnsubrg  16747  mulgrhm2  16776  znrrg  16834  ocvocv  16886  ocv2ss  16888  ocvin  16889  lsmcss  16907  cssmre  16908  pjfo  16930  pjcss  16931  obs2ss  16944  bastg  17019  tgss  17021  tgtop  17026  tgidm  17033  en2top  17038  neisspw  17159  topssnei  17176  neiptopuni  17182  lpss3  17196  clslp  17200  tgrest  17211  ssrest  17228  restfpw  17231  restntr  17234  ordtbas2  17243  ordtbas  17244  cnss1  17328  cnss2  17329  cnsscnp  17331  cnrest2r  17339  cmpsublem  17450  cmpsub  17451  tgcmp  17452  cmpcld  17453  hauscmplem  17457  cnconn  17473  2ndcsep  17510  llyss  17530  nllyss  17531  restnlly  17533  restlly  17534  kgenss  17563  kgenidm  17567  llycmpkgen2  17570  1stckgen  17574  kgen2ss  17575  kgencn3  17578  ptbasfi  17601  ptpjopn  17632  ptclsg  17635  txdis  17652  txkgen  17672  xkoptsub  17674  xkopjcn  17676  txcon  17709  qtoptop2  17719  qtopuni  17722  qtopkgen  17730  basqtop  17731  tgqtop  17732  qtopss  17735  qtoprest  17737  qtopomap  17738  qtopcmap  17739  kqsat  17751  kqcldsat  17753  hmphdis  17816  isfild  17878  ssfg  17892  fgss  17893  fgss2  17894  fgfil  17895  fgabs  17899  filcon  17903  fgtr  17910  trfg  17911  uzrest  17917  ufilmax  17927  ufileu  17939  filufint  17940  rnelfm  17973  fmfnfmlem2  17975  fmfnfmlem4  17977  flimss2  17992  flimss1  17993  flimclsi  17998  flimcf  18002  flimsncls  18006  fclssscls  18038  fclsss1  18042  fclsss2  18043  fclscf  18045  uffclsflim  18051  alexsublem  18063  alexsubALTlem3  18068  ptcmplem2  18072  ptcmplem3  18073  cnextf  18085  symgtgp  18119  cldsubg  18128  tsmscl  18152  haustsms2  18154  tgptsmscls  18167  tsmsxp  18172  restutop  18255  restutopopn  18256  ustuqtop4  18262  utop2nei  18268  utop3cls  18269  ucncn  18303  xblss2ps  18419  xblss2  18420  unirnblps  18437  unirnbl  18438  xrsblre  18830  xrsmopn  18831  recld2  18833  zdis  18835  icccmplem2  18842  cncfss  18917  cnheiborlem  18967  htpycn  18986  phtpyhtpy  18995  pi1blem  19052  clsocv  19192  cfilfcls  19215  iscmet3lem2  19233  iscmet2  19235  caussi  19238  equivcfil  19240  lmcau  19253  cmetss  19255  pjth  19328  hlhil  19332  ivthicc  19343  ovoliunnul  19391  ovolicopnf  19408  uniioombllem3  19465  dyadmbllem  19479  opnmbllem  19481  volsup2  19485  vitalilem2  19489  itg1addlem4  19579  itg10a  19590  itg1ge0a  19591  mbfi1fseqlem4  19598  itg2gt0  19640  limciun  19769  perfdvf  19778  dvidlem  19790  cpnord  19809  dvaddf  19816  dvmulf  19817  dvcof  19822  dvcj  19824  dvrec  19829  dvcnv  19849  dvlip2  19867  dvivth  19882  dvne0  19883  dvcnvre  19891  ftc1cn  19915  ply1lpir  20089  plyco0  20099  plyexmo  20218  ulmdv  20307  pserdv  20333  abelth  20345  efif1o  20436  logno1  20515  efopnlem2  20536  loglesqr  20630  ppisval  20874  ppisval2  20875  ppinprm  20923  chtnprm  20925  fsumvma  20985  dchrfi  21027  chtppilimlem2  21156  chebbnd2  21159  vmadivsumb  21165  rplogsumlem2  21167  dchrisumlem2  21172  vmalogdivsum2  21220  vmalogdivsum  21221  2vmadivsumlem  21222  selbergb  21231  selberg2b  21234  selberg3lem1  21239  selberg3lem2  21240  selberg3  21241  selberg4lem1  21242  selberg4  21243  pntrlog2bndlem2  21260  pntrlog2bndlem4  21262  sizeusglecusglem1  21481  ococss  22783  shsub1  22814  shless  22849  shmodsi  22879  pjhth  22883  spansnss  23061  spanpr  23070  spansnm0i  23140  pjjsi  23190  sumdmdii  23906  sumdmdlem  23909  sumdmdlem2  23910  cdj3lem1  23925  abrexss  23981  rnmpt2ss  24074  ssnnssfz  24136  kerf1hrm  24250  tpr2rico  24298  esumpcvgval  24456  cldssbrsiga  24529  measdivcstOLD  24566  mbfmcnt  24606  dya2iocuni  24621  lgamcvg2  24827  sconpi1  24914  cvmscld  24948  cvmsss2  24949  cvmliftlem15  24973  rtrclreclem.trans  25134  prodmolem2a  25249  fprod2dlem  25293  fprodcom2  25297  dfon2lem6  25399  predpo  25439  preddowncl  25451  wfrlem10  25520  nofulllem5  25615  supaddc  26184  supadd  26185  mblfinlem  26190  ftc1cnnc  26225  fnessref  26310  locfincmp  26321  locfincf  26323  fgmin  26336  tailfb  26343  sstotbnd3  26422  prdstotbnd  26440  cntotbnd  26442  ismtyhmeo  26451  1idl  26573  eldiophss  26770  rencldnfilem  26818  pellexlem5  26833  pell14qrss1234  26856  pell1qrss14  26868  pellfundre  26881  pellfundge  26882  pellfundlb  26884  pellfundglb  26885  harinf  27042  kercvrlsm  27096  pwssplit4  27106  frlmsslsp  27163  lindfrn  27206  hbtlem5  27247  proot1hash  27434  refsumcn  27615  stoweidlem27  27690  stoweidlem46  27709  stoweidlem57  27720  ffnafv  27949  trsspwALT3  28787  sspwimpALT2  28895  bnj1033  29192  bnj1398  29257  lshpdisj  29624  lssats  29649  lkrlsp  29739  lkrin  29801  glbconxN  30014  paddss1  30453  paddss2  30454  paddasslem16  30471  paddidm  30477  pmodlem2  30483  pmapjoin  30488  pmapjat1  30489  pclfinN  30536  pclfinclN  30586  cdleme50rnlem  31180  diasslssN  31696  dia2dimlem12  31712  dihsslss  31913  baerlem3lem2  32347  baerlem5alem2  32348  baerlem5blem2  32349  hdmaprnN  32504  hgmaprnN  32541
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator