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

Theorem ssrdv 3357
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 1685 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3340 . 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 1367    e. wcel 1756    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337
This theorem is referenced by:  sscon  3485  ssdif  3486  unss1  3520  ssrin  3570  eq0rdv  3667  uniss  4107  intss1  4138  intmin  4143  intssuni  4145  iunss1  4177  iinss1  4178  ss2iun  4181  ssiun  4207  ssiun2  4208  iinss  4216  iinss2  4217  trintss  4396  sspwb  4536  pwssun  4622  tron  4737  tz7.7  4740  xpsspw  4948  relop  4985  dmss  5034  dmcosseq  5096  ssrnres  5271  sossfld  5280  dffv2  5759  chfnrn  5809  suppssOLD  5831  dff3  5851  ffnfv  5864  f1imass  5972  ssorduni  6392  onint  6401  limsssuc  6456  limuni3  6458  limomss  6476  fo1stres  6595  fo2ndres  6596  fo2ndf  6674  fnse  6684  ressuppssdif  6705  suppss  6714  reldmtpos  6748  onfununi  6794  smoiun  6814  smorndom  6821  tz7.48-1  6890  tz7.49  6892  oaass  6992  qsss  7153  uniinqs  7172  pmss12g  7231  mapss  7247  ixpssmap2g  7284  ixpssmapg  7285  fineqv  7520  pssnn  7523  ssfii  7661  dffi2  7665  ordtypelem9  7732  ordtypelem10  7733  oismo  7746  unxpwdom2  7795  inf3lemd  7825  inf3lem1  7826  inf3lem6  7831  cantnflem3  7891  cantnf  7893  cantnflem3OLD  7913  cantnfOLD  7915  cnfcom3lem  7928  cnfcom3lemOLD  7936  onssr1  8030  rankunb  8049  tcrank  8083  harcard  8140  carduni  8143  infxpenlem  8172  infpwfien  8224  dfac12r  8307  ackbij2lem1  8380  ackbij1lem18  8398  isfin1-3  8547  fin1a2lem11  8571  fin1a2lem13  8573  zorn2lem4  8660  zorn2lem5  8661  ttukeylem6  8675  ttukeylem7  8676  fpwwe2lem11  8799  fpwwe2lem12  8800  fpwwe2  8802  wunr1om  8878  wunom  8879  tskr1om  8926  tskr1om2  8927  tskxpss  8931  tskcard  8940  tskuni  8942  grothomex  8988  genpss  9165  distrlem1pr  9186  distrlem5pr  9188  prlem934  9194  ltexprlem2  9198  ltexprlem6  9202  ltexprlem7  9203  reclem3pr  9210  reclem4pr  9211  supmul1  10287  supmullem2  10289  peano5uzi  10722  uzss  10873  ixxdisj  11307  ixxss1  11310  ixxss2  11311  ixxss12  11312  ixxub  11313  ixxlb  11314  iocssre  11367  icossre  11368  iccssre  11369  icodisj  11402  fzss1  11489  fzss2  11490  fzosplit  11574  fzouzsplit  11576  ssfzo12bi  11614  sswrd  12234  isercoll  13137  summolem2a  13184  fsumcvg3  13198  fsum2dlem  13229  fsumcom2  13233  qshash  13282  bitsfzo  13623  phimullem  13846  prmreclem5  13973  1arith  13980  vdwlem2  14035  vdwlem6  14039  vdwlem8  14041  ramtlecl  14053  monhom  14666  epihom  14673  funcsetcres2  14953  psdmrn  15369  psssdm2  15377  gsumwspan  15515  frmdss2  15532  ssnmz  15714  conjnmz  15771  gex1  16081  sylow2alem1  16107  sylow3lem3  16119  lsmless1x  16134  lsmless2x  16135  lsmub1x  16136  lsmub2x  16137  lsmmod  16163  lsmdisj2  16170  efgrelexlemb  16238  efgcpbllemb  16243  cntzcmn  16315  gsum2d2  16456  dprdub  16512  dprdss  16516  dprddisj2  16527  dprddisj2OLD  16528  ablfacrp  16557  pgpfac1lem3  16568  isdrng2  16822  subrguss  16860  subrgmre  16869  lssssr  17014  lsssssubg  17019  lssmre  17027  lbspss  17143  lspdisj  17186  lbsextlem2  17220  lidl1el  17280  drngnidl  17291  lpiss  17312  unitrrg  17345  fidomndrng  17359  mplbas2  17531  mplbas2OLD  17532  zsssubrg  17851  qsssubdrg  17852  cnsubrg  17853  mulgrhm2  17907  mulgrhm2OLD  17910  znrrg  17978  ocvocv  18076  ocv2ss  18078  ocvin  18079  lsmcss  18097  cssmre  18098  pjfo  18120  pjcss  18121  obs2ss  18134  frlmsslsp  18203  frlmsslspOLD  18204  lindfrn  18230  bastg  18551  tgss  18553  tgtop  18558  tgidm  18565  en2top  18570  neisspw  18691  topssnei  18708  neiptopuni  18714  lpss3  18728  clslp  18732  tgrest  18743  ssrest  18760  restfpw  18763  restntr  18766  ordtbas2  18775  ordtbas  18776  cnss1  18860  cnss2  18861  cnsscnp  18863  cnrest2r  18871  cmpsublem  18982  cmpsub  18983  tgcmp  18984  cmpcld  18985  hauscmplem  18989  cnconn  19006  2ndcsep  19043  llyss  19063  nllyss  19064  restnlly  19066  restlly  19067  kgenss  19096  kgenidm  19100  llycmpkgen2  19103  1stckgen  19107  kgen2ss  19108  kgencn3  19111  ptbasfi  19134  ptpjopn  19165  ptclsg  19168  txdis  19185  txkgen  19205  xkoptsub  19207  xkopjcn  19209  txcon  19242  qtoptop2  19252  qtopuni  19255  qtopkgen  19263  basqtop  19264  tgqtop  19265  qtopss  19268  qtoprest  19270  qtopomap  19271  qtopcmap  19272  kqsat  19284  kqcldsat  19286  hmphdis  19349  isfild  19411  ssfg  19425  fgss  19426  fgss2  19427  fgfil  19428  fgabs  19432  filcon  19436  fgtr  19443  trfg  19444  uzrest  19450  ufilmax  19460  ufileu  19472  filufint  19473  rnelfm  19506  fmfnfmlem2  19508  fmfnfmlem4  19510  flimss2  19525  flimss1  19526  flimclsi  19531  flimcf  19535  flimsncls  19539  fclssscls  19571  fclsss1  19575  fclsss2  19576  fclscf  19578  uffclsflim  19584  alexsublem  19596  alexsubALTlem3  19601  ptcmplem2  19605  ptcmplem3  19606  cnextf  19618  symgtgp  19652  cldsubg  19661  tsmscl  19685  haustsms2  19687  tgptsmscls  19704  tsmsxp  19709  restutop  19792  restutopopn  19793  ustuqtop4  19799  utop2nei  19805  utop3cls  19806  ucncn  19840  xblss2ps  19956  xblss2  19957  unirnblps  19974  unirnbl  19975  xrsblre  20368  xrsmopn  20369  recld2  20371  zdis  20373  icccmplem2  20380  cncfss  20455  cnheiborlem  20506  htpycn  20525  phtpyhtpy  20534  pi1blem  20591  clsocv  20742  cfilfcls  20765  iscmet3lem2  20783  iscmet2  20785  caussi  20788  equivcfil  20790  lmcau  20803  cmetss  20805  pjth  20906  hlhil  20910  ivthicc  20922  ovoliunnul  20970  ovolicopnf  20987  uniioombllem3  21045  dyadmbllem  21059  opnmbllem  21061  volsup2  21065  vitalilem2  21069  itg1addlem4  21157  itg10a  21168  itg1ge0a  21169  mbfi1fseqlem4  21176  itg2gt0  21218  limciun  21349  perfdvf  21358  dvidlem  21370  cpnord  21389  dvaddf  21396  dvmulf  21397  dvcof  21402  dvcj  21404  dvrec  21409  dvcnv  21429  dvlip2  21447  dvivth  21462  dvne0  21463  dvcnvre  21471  ftc1cn  21495  ply1lpir  21630  plyco0  21640  plyexmo  21759  ulmdv  21848  pserdv  21874  abelth  21886  efif1o  21982  logno1  22061  efopnlem2  22082  loglesqr  22176  ppisval  22421  ppisval2  22422  ppinprm  22470  chtnprm  22472  fsumvma  22532  dchrfi  22574  chtppilimlem2  22703  chebbnd2  22706  vmadivsumb  22712  rplogsumlem2  22714  dchrisumlem2  22719  vmalogdivsum2  22767  vmalogdivsum  22768  2vmadivsumlem  22769  selbergb  22778  selberg2b  22781  selberg3lem1  22786  selberg3lem2  22787  selberg3  22788  selberg4lem1  22789  selberg4  22790  pntrlog2bndlem2  22807  pntrlog2bndlem4  22809  sizeusglecusglem1  23360  ococss  24664  shsub1  24695  shless  24730  shmodsi  24760  pjhth  24764  spansnss  24942  spanpr  24951  spansnm0i  25021  pjjsi  25071  sumdmdii  25787  sumdmdlem  25790  sumdmdlem2  25791  cdj3lem1  25806  abrexss  25861  rnmpt2ss  25960  unifi3  25973  ssnnssfz  26044  kerf1hrm  26260  tpr2rico  26311  esumpcvgval  26496  cldssbrsiga  26570  measdivcstOLD  26607  mbfmcnt  26652  dya2iocuni  26667  oddpwdc  26706  eulerpartlemgs2  26732  lgamcvg2  27010  sconpi1  27097  cvmscld  27131  cvmsss2  27132  cvmliftlem15  27156  rtrclreclem.trans  27317  prodmolem2a  27416  fprod2dlem  27460  fprodcom2  27464  dfon2lem6  27570  predpo  27614  preddowncl  27626  wfrlem10  27702  nofulllem5  27816  supaddc  28388  supadd  28389  opnmbllem0  28398  ftc1cnnc  28437  fnessref  28536  locfincmp  28547  locfincf  28549  fgmin  28562  tailfb  28569  sstotbnd3  28646  prdstotbnd  28664  cntotbnd  28666  ismtyhmeo  28675  1idl  28797  eldiophss  29084  rencldnfilem  29130  pellexlem5  29145  pell14qrss1234  29168  pell1qrss14  29180  pellfundre  29193  pellfundge  29194  pellfundlb  29196  pellfundglb  29197  harinf  29354  kercvrlsm  29407  pwssplit4  29413  hbtlem5  29455  proot1hash  29539  refsumcn  29723  stoweidlem27  29793  stoweidlem46  29812  stoweidlem57  29823  ffnafv  30048  ssnn0ssfz  30711  suppssfz  30755  fsuppmapnn0fiub  30768  scmatsgrp1  30849  lincolss  30899  lcoss  30901  lcosslsp  30903  trsspwALT3  31483  sspwimpALT2  31593  bnj1033  31889  bnj1398  31954  lshpdisj  32525  lssats  32550  lkrlsp  32640  lkrin  32702  glbconxN  32915  paddss1  33354  paddss2  33355  paddasslem16  33372  paddidm  33378  pmodlem2  33384  pmapjoin  33389  pmapjat1  33390  pclfinN  33437  pclfinclN  33487  cdleme50rnlem  34081  diasslssN  34597  dia2dimlem12  34613  dihsslss  34814  baerlem3lem2  35248  baerlem5alem2  35249  baerlem5blem2  35250  hdmaprnN  35405  hgmaprnN  35442
  Copyright terms: Public domain W3C validator