MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssrdv Structured version   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  4758  onint  4767  limsssuc  4822  limuni3  4824  limomss  4842  xpsspw  4978  relop  5015  dmss  5061  dmcosseq  5129  ssrnres  5301  sossfld  5309  dffv2  5788  chfnrn  5833  suppss  5855  dff3  5874  ffnfv  5886  f1imass  6002  fo1stres  6362  fo2ndres  6363  fo2ndf  6445  fnse  6455  reldmtpos  6479  onfununi  6595  smoiun  6615  smorndom  6622  tz7.48-1  6692  tz7.49  6694  oaass  6796  qsss  6957  uniinqs  6976  pmss12g  7032  mapss  7048  ixpssmap2g  7083  ixpssmapg  7084  fineqv  7316  pssnn  7319  ssfii  7416  dffi2  7420  ordtypelem9  7487  ordtypelem10  7488  oismo  7501  unxpwdom2  7548  inf3lemd  7574  inf3lem1  7575  inf3lem6  7580  cantnflem3  7639  cantnf  7641  cnfcom3lem  7652  onssr1  7749  rankunb  7768  tcrank  7800  harcard  7857  carduni  7860  infxpenlem  7887  infpwfien  7935  dfac12r  8018  ackbij2lem1  8091  ackbij1lem18  8109  isfin1-3  8258  fin1a2lem11  8282  fin1a2lem13  8284  zorn2lem4  8371  zorn2lem5  8372  ttukeylem6  8386  ttukeylem7  8387  fpwwe2lem11  8507  fpwwe2lem12  8508  fpwwe2  8510  wunr1om  8586  wunom  8587  tskr1om  8634  tskr1om2  8635  tskxpss  8639  tskcard  8648  tskuni  8650  grothomex  8696  genpss  8873  distrlem1pr  8894  distrlem5pr  8896  prlem934  8902  ltexprlem2  8906  ltexprlem6  8910  ltexprlem7  8911  reclem3pr  8918  reclem4pr  8919  supmul1  9965  supmullem2  9967  peano5uzi  10350  uzss  10498  ixxdisj  10923  ixxss1  10926  ixxss2  10927  ixxss12  10928  ixxub  10929  ixxlb  10930  iocssre  10982  icossre  10983  iccssre  10984  icodisj  11014  fzss1  11083  fzss2  11084  fzosplit  11158  fzouzsplit  11160  sswrd  11729  isercoll  12453  summolem2a  12501  fsumcvg3  12515  fsum2dlem  12546  fsumcom2  12550  qshash  12598  bitsfzo  12939  phimullem  13160  prmreclem5  13280  1arith  13287  vdwlem2  13342  vdwlem6  13346  vdwlem8  13348  ramtlecl  13360  monhom  13953  epihom  13960  funcsetcres2  14240  psdmrn  14631  psssdm2  14639  gsumwspan  14783  frmdss2  14800  ssnmz  14974  conjnmz  15031  gex1  15217  sylow2alem1  15243  sylow3lem3  15255  lsmless1x  15270  lsmless2x  15271  lsmub1x  15272  lsmub2x  15273  lsmmod  15299  lsmdisj2  15306  efgrelexlemb  15374  efgcpbllemb  15379  cntzcmn  15451  gsum2d2  15540  dprdub  15575  dprdss  15579  dprddisj2  15589  ablfacrp  15616  pgpfac1lem3  15627  isdrng2  15837  subrguss  15875  subrgmre  15884  lssssr  16021  lsssssubg  16026  lssmre  16034  lbspss  16146  lspdisj  16189  lbsextlem2  16223  lidl1el  16281  drngnidl  16292  lpiss  16313  unitrrg  16345  fidomndrng  16359  mplbas2  16523  zsssubrg  16749  qsssubdrg  16750  cnsubrg  16751  mulgrhm2  16780  znrrg  16838  ocvocv  16890  ocv2ss  16892  ocvin  16893  lsmcss  16911  cssmre  16912  pjfo  16934  pjcss  16935  obs2ss  16948  bastg  17023  tgss  17025  tgtop  17030  tgidm  17037  en2top  17042  neisspw  17163  topssnei  17180  neiptopuni  17186  lpss3  17200  clslp  17204  tgrest  17215  ssrest  17232  restfpw  17235  restntr  17238  ordtbas2  17247  ordtbas  17248  cnss1  17332  cnss2  17333  cnsscnp  17335  cnrest2r  17343  cmpsublem  17454  cmpsub  17455  tgcmp  17456  cmpcld  17457  hauscmplem  17461  cnconn  17477  2ndcsep  17514  llyss  17534  nllyss  17535  restnlly  17537  restlly  17538  kgenss  17567  kgenidm  17571  llycmpkgen2  17574  1stckgen  17578  kgen2ss  17579  kgencn3  17582  ptbasfi  17605  ptpjopn  17636  ptclsg  17639  txdis  17656  txkgen  17676  xkoptsub  17678  xkopjcn  17680  txcon  17713  qtoptop2  17723  qtopuni  17726  qtopkgen  17734  basqtop  17735  tgqtop  17736  qtopss  17739  qtoprest  17741  qtopomap  17742  qtopcmap  17743  kqsat  17755  kqcldsat  17757  hmphdis  17820  isfild  17882  ssfg  17896  fgss  17897  fgss2  17898  fgfil  17899  fgabs  17903  filcon  17907  fgtr  17914  trfg  17915  uzrest  17921  ufilmax  17931  ufileu  17943  filufint  17944  rnelfm  17977  fmfnfmlem2  17979  fmfnfmlem4  17981  flimss2  17996  flimss1  17997  flimclsi  18002  flimcf  18006  flimsncls  18010  fclssscls  18042  fclsss1  18046  fclsss2  18047  fclscf  18049  uffclsflim  18055  alexsublem  18067  alexsubALTlem3  18072  ptcmplem2  18076  ptcmplem3  18077  cnextf  18089  symgtgp  18123  cldsubg  18132  tsmscl  18156  haustsms2  18158  tgptsmscls  18171  tsmsxp  18176  restutop  18259  restutopopn  18260  ustuqtop4  18266  utop2nei  18272  utop3cls  18273  ucncn  18307  xblss2ps  18423  xblss2  18424  unirnblps  18441  unirnbl  18442  xrsblre  18834  xrsmopn  18835  recld2  18837  zdis  18839  icccmplem2  18846  cncfss  18921  cnheiborlem  18971  htpycn  18990  phtpyhtpy  18999  pi1blem  19056  clsocv  19196  cfilfcls  19219  iscmet3lem2  19237  iscmet2  19239  caussi  19242  equivcfil  19244  lmcau  19257  cmetss  19259  pjth  19332  hlhil  19336  ivthicc  19347  ovoliunnul  19395  ovolicopnf  19412  uniioombllem3  19469  dyadmbllem  19483  opnmbllem  19485  volsup2  19489  vitalilem2  19493  itg1addlem4  19583  itg10a  19594  itg1ge0a  19595  mbfi1fseqlem4  19602  itg2gt0  19644  limciun  19773  perfdvf  19782  dvidlem  19794  cpnord  19813  dvaddf  19820  dvmulf  19821  dvcof  19826  dvcj  19828  dvrec  19833  dvcnv  19853  dvlip2  19871  dvivth  19886  dvne0  19887  dvcnvre  19895  ftc1cn  19919  ply1lpir  20093  plyco0  20103  plyexmo  20222  ulmdv  20311  pserdv  20337  abelth  20349  efif1o  20440  logno1  20519  efopnlem2  20540  loglesqr  20634  ppisval  20878  ppisval2  20879  ppinprm  20927  chtnprm  20929  fsumvma  20989  dchrfi  21031  chtppilimlem2  21160  chebbnd2  21163  vmadivsumb  21169  rplogsumlem2  21171  dchrisumlem2  21176  vmalogdivsum2  21224  vmalogdivsum  21225  2vmadivsumlem  21226  selbergb  21235  selberg2b  21238  selberg3lem1  21243  selberg3lem2  21244  selberg3  21245  selberg4lem1  21246  selberg4  21247  pntrlog2bndlem2  21264  pntrlog2bndlem4  21266  sizeusglecusglem1  21485  ococss  22787  shsub1  22818  shless  22853  shmodsi  22883  pjhth  22887  spansnss  23065  spanpr  23074  spansnm0i  23144  pjjsi  23194  sumdmdii  23910  sumdmdlem  23913  sumdmdlem2  23914  cdj3lem1  23929  abrexss  23985  rnmpt2ss  24078  ssnnssfz  24140  kerf1hrm  24254  tpr2rico  24302  esumpcvgval  24460  cldssbrsiga  24533  measdivcstOLD  24570  mbfmcnt  24610  dya2iocuni  24625  lgamcvg2  24831  sconpi1  24918  cvmscld  24952  cvmsss2  24953  cvmliftlem15  24977  rtrclreclem.trans  25138  prodmolem2a  25252  fprod2dlem  25296  fprodcom2  25300  dfon2lem6  25407  predpo  25451  preddowncl  25463  wfrlem10  25539  nofulllem5  25653  supaddc  26228  supadd  26229  mblfinlem  26234  ftc1cnnc  26269  fnessref  26364  locfincmp  26375  locfincf  26377  fgmin  26390  tailfb  26397  sstotbnd3  26476  prdstotbnd  26494  cntotbnd  26496  ismtyhmeo  26505  1idl  26627  eldiophss  26824  rencldnfilem  26872  pellexlem5  26887  pell14qrss1234  26910  pell1qrss14  26922  pellfundre  26935  pellfundge  26936  pellfundlb  26938  pellfundglb  26939  harinf  27096  kercvrlsm  27149  pwssplit4  27159  frlmsslsp  27216  lindfrn  27259  hbtlem5  27300  proot1hash  27487  refsumcn  27668  stoweidlem27  27743  stoweidlem46  27762  stoweidlem57  27773  ffnafv  28002  trsspwALT3  28870  sspwimpALT2  28977  bnj1033  29275  bnj1398  29340  lshpdisj  29722  lssats  29747  lkrlsp  29837  lkrin  29899  glbconxN  30112  paddss1  30551  paddss2  30552  paddasslem16  30569  paddidm  30575  pmodlem2  30581  pmapjoin  30586  pmapjat1  30587  pclfinN  30634  pclfinclN  30684  cdleme50rnlem  31278  diasslssN  31794  dia2dimlem12  31810  dihsslss  32011  baerlem3lem2  32445  baerlem5alem2  32446  baerlem5blem2  32447  hdmaprnN  32602  hgmaprnN  32639
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