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

Theorem ssrdv 3509
Description: Deduction rule based on subclass definition. (Contributed by NM, 15-Nov-1995.)
Hypothesis
Ref Expression
ssrdv.1
Assertion
Ref Expression
ssrdv
Distinct variable groups:   ,   ,   ,

Proof of Theorem ssrdv
StepHypRef Expression
1 ssrdv.1 . . 3
21alrimiv 1719 . 2
3 dfss2 3492 . 2
42, 3sylibr 212 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393  e.wcel 1818  C_wss 3475
This theorem is referenced by:  sscon  3637  ssdif  3638  unss1  3672  ssrin  3722  eq0rdv  3820  uniss  4270  intss1  4301  intmin  4306  intssuni  4309  iunss1  4342  iinss1  4343  ss2iun  4346  ssiun  4372  ssiun2  4373  iinss  4381  iinss2  4382  trintss  4561  sspwb  4701  pwssun  4791  tron  4906  tz7.7  4909  xpsspw  5121  relop  5158  dmss  5207  dmcosseq  5269  ssrnres  5450  sossfld  5459  dffv2  5946  chfnrn  5998  suppssOLD  6020  fvn0ssdmfun  6022  fveqdmss  6026  dff3  6044  ffnfv  6057  f1imass  6172  ssorduni  6621  onint  6630  limsssuc  6685  limuni3  6687  limomss  6705  fo1stres  6824  fo2ndres  6825  fo2ndf  6907  fnse  6917  ressuppssdif  6940  suppss  6949  reldmtpos  6982  onfununi  7031  smoiun  7051  smorndom  7058  tz7.48-1  7127  tz7.49  7129  oaass  7229  qsss  7391  uniinqs  7410  pmss12g  7465  mapss  7481  ixpssmap2g  7518  ixpssmapg  7519  fineqv  7755  pssnn  7758  ssfii  7899  dffi2  7903  ordtypelem9  7972  ordtypelem10  7973  oismo  7986  unxpwdom2  8035  inf3lemd  8065  inf3lem1  8066  inf3lem6  8071  cantnflem3  8131  cantnf  8133  cantnflem3OLD  8153  cantnfOLD  8155  cnfcom3lem  8168  cnfcom3lemOLD  8176  onssr1  8270  rankunb  8289  tcrank  8323  harcard  8380  carduni  8383  infxpenlem  8412  infpwfien  8464  dfac12r  8547  ackbij2lem1  8620  ackbij1lem18  8638  isfin1-3  8787  fin1a2lem11  8811  fin1a2lem13  8813  zorn2lem4  8900  zorn2lem5  8901  ttukeylem6  8915  ttukeylem7  8916  fpwwe2lem11  9039  fpwwe2lem12  9040  fpwwe2  9042  wunr1om  9118  wunom  9119  tskr1om  9166  tskr1om2  9167  tskxpss  9171  tskcard  9180  tskuni  9182  grothomex  9228  genpss  9403  distrlem1pr  9424  distrlem5pr  9426  prlem934  9432  ltexprlem2  9436  ltexprlem6  9440  ltexprlem7  9441  reclem3pr  9448  reclem4pr  9449  supmul1  10533  supmullem2  10535  peano5uzi  10976  uzss  11130  ixxdisj  11573  ixxss1  11576  ixxss2  11577  ixxss12  11578  ixxub  11579  ixxlb  11580  iocssre  11633  icossre  11634  iccssre  11635  icodisj  11674  fzss1  11751  fzss2  11752  fzosplit  11858  fzouzsplit  11860  ssfzo12bi  11907  ssnn0fi  12094  fsuppmapnn0fiub  12097  suppssfz  12100  sswrd  12555  isercoll  13490  summolem2a  13537  fsumcvg3  13551  fsum2dlem  13585  fsumcom2  13589  qshash  13639  prodmolem2a  13741  fprod2dlem  13784  fprodcom2  13788  bitsfzo  14085  phimullem  14309  prmreclem5  14438  1arith  14445  vdwlem2  14500  vdwlem6  14504  vdwlem8  14506  ramtlecl  14518  monhom  15130  epihom  15137  funcsetcres2  15420  psdmrn  15837  psssdm2  15845  gsumwspan  16014  frmdss2  16031  ssnmz  16243  conjnmz  16300  gex1  16611  sylow2alem1  16637  sylow3lem3  16649  lsmless1x  16664  lsmless2x  16665  lsmub1x  16666  lsmub2x  16667  lsmmod  16693  lsmdisj2  16700  efgrelexlemb  16768  efgcpbllemb  16773  cntzcmn  16848  gsum2d2  17002  dprdub  17072  dprdss  17076  dprddisj2  17087  dprddisj2OLD  17088  ablfacrp  17117  pgpfac1lem3  17128  kerf1hrm  17392  isdrng2  17406  subrguss  17444  subrgmre  17453  lssssr  17599  lsssssubg  17604  lssmre  17612  lbspss  17728  lspdisj  17771  lbsextlem2  17805  lidl1el  17866  drngnidl  17877  lpiss  17898  unitrrg  17942  fidomndrng  17956  mplbas2  18134  mplbas2OLD  18135  zsssubrg  18476  qsssubdrg  18477  cnsubrg  18478  mulgrhm2  18533  mulgrhm2OLD  18536  znrrg  18604  ocvocv  18702  ocv2ss  18704  ocvin  18705  lsmcss  18723  cssmre  18724  pjfo  18746  pjcss  18747  obs2ss  18760  frlmsslsp  18829  frlmsslspOLD  18830  lindfrn  18856  dmatsgrp  19001  scmatsgrp  19021  scmatsgrp1  19024  m2cpmrngiso  19259  bastg  19467  tgss  19470  tgtop  19475  tgidm  19482  en2top  19487  neisspw  19608  topssnei  19625  neiptopuni  19631  lpss3  19645  clslp  19649  tgrest  19660  ssrest  19677  restfpw  19680  restntr  19683  ordtbas2  19692  ordtbas  19693  cnss1  19777  cnss2  19778  cnsscnp  19780  cnrest2r  19788  cmpsublem  19899  cmpsub  19900  tgcmp  19901  cmpcld  19902  hauscmplem  19906  cnconn  19923  2ndcsep  19960  llyss  19980  nllyss  19981  restnlly  19983  restlly  19984  locfincmp  20027  locfincf  20032  kgenss  20044  kgenidm  20048  llycmpkgen2  20051  1stckgen  20055  kgen2ss  20056  kgencn3  20059  ptbasfi  20082  ptpjopn  20113  ptclsg  20116  txdis  20133  txkgen  20153  xkoptsub  20155  xkopjcn  20157  txcon  20190  qtoptop2  20200  qtopuni  20203  qtopkgen  20211  basqtop  20212  tgqtop  20213  qtopss  20216  qtoprest  20218  qtopomap  20219  qtopcmap  20220  kqsat  20232  kqcldsat  20234  hmphdis  20297  isfild  20359  ssfg  20373  fgss  20374  fgss2  20375  fgfil  20376  fgabs  20380  filcon  20384  fgtr  20391  trfg  20392  uzrest  20398  ufilmax  20408  ufileu  20420  filufint  20421  rnelfm  20454  fmfnfmlem2  20456  fmfnfmlem4  20458  flimss2  20473  flimss1  20474  flimclsi  20479  flimcf  20483  flimsncls  20487  fclssscls  20519  fclsss1  20523  fclsss2  20524  fclscf  20526  uffclsflim  20532  alexsublem  20544  alexsubALTlem3  20549  ptcmplem2  20553  ptcmplem3  20554  cnextf  20566  symgtgp  20600  cldsubg  20609  tsmscl  20633  haustsms2  20635  tgptsmscls  20652  tsmsxp  20657  restutop  20740  restutopopn  20741  ustuqtop4  20747  utop2nei  20753  utop3cls  20754  ucncn  20788  xblss2ps  20904  xblss2  20905  unirnblps  20922  unirnbl  20923  xrsblre  21316  xrsmopn  21317  recld2  21319  zdis  21321  icccmplem2  21328  cncfss  21403  cnheiborlem  21454  htpycn  21473  phtpyhtpy  21482  pi1blem  21539  clsocv  21690  cfilfcls  21713  iscmet3lem2  21731  iscmet2  21733  caussi  21736  equivcfil  21738  lmcau  21751  cmetss  21753  pjth  21854  hlhil  21858  ivthicc  21870  ovoliunnul  21918  ovolicopnf  21935  uniioombllem3  21994  dyadmbllem  22008  opnmbllem  22010  volsup2  22014  vitalilem2  22018  itg1addlem4  22106  itg10a  22117  itg1ge0a  22118  mbfi1fseqlem4  22125  itg2gt0  22167  limciun  22298  perfdvf  22307  dvidlem  22319  cpnord  22338  dvaddf  22345  dvmulf  22346  dvcof  22351  dvcj  22353  dvrec  22358  dvcnv  22378  dvlip2  22396  dvivth  22411  dvne0  22412  dvcnvre  22420  ftc1cn  22444  ply1lpir  22579  plyco0  22589  plyexmo  22709  ulmdv  22798  pserdv  22824  abelth  22836  efif1o  22933  logno1  23017  efopnlem2  23038  loglesqrt  23132  ppisval  23377  ppisval2  23378  ppinprm  23426  chtnprm  23428  fsumvma  23488  dchrfi  23530  chtppilimlem2  23659  chebbnd2  23662  vmadivsumb  23668  rplogsumlem2  23670  dchrisumlem2  23675  vmalogdivsum2  23723  vmalogdivsum  23724  2vmadivsumlem  23725  selbergb  23734  selberg2b  23737  selberg3lem1  23742  selberg3lem2  23743  selberg3  23744  selberg4lem1  23745  selberg4  23746  pntrlog2bndlem2  23763  pntrlog2bndlem4  23765  sizeusglecusglem1  24484  clwwlkssclwwlkn  24792  ococss  26211  shsub1  26242  shless  26277  shmodsi  26307  pjhth  26311  spansnss  26489  spanpr  26498  spansnm0i  26568  pjjsi  26618  sumdmdii  27334  sumdmdlem  27337  sumdmdlem2  27338  cdj3lem1  27353  abrexss  27410  rnmpt2ss  27515  unifi3  27528  ssnnssfz  27597  reff  27842  crefss  27852  cmpcref  27853  tpr2rico  27894  esumpcvgval  28084  cldssbrsiga  28158  measdivcstOLD  28195  mbfmcnt  28239  dya2iocuni  28254  oddpwdc  28293  eulerpartlemgs2  28319  lgamcvg2  28597  sconpi1  28684  cvmscld  28718  cvmsss2  28719  cvmliftlem15  28743  rtrclreclem.trans  29069  dfon2lem6  29220  predpo  29264  preddowncl  29276  wfrlem10  29352  nofulllem5  29466  supaddc  30041  supadd  30042  opnmbllem0  30050  ftc1cnnc  30089  fnessref  30175  fgmin  30188  tailfb  30195  sstotbnd3  30272  prdstotbnd  30290  cntotbnd  30292  ismtyhmeo  30301  1idl  30423  eldiophss  30708  rencldnfilem  30754  pellexlem5  30769  pell14qrss1234  30792  pell1qrss14  30804  pellfundre  30817  pellfundge  30818  pellfundlb  30820  pellfundglb  30821  harinf  30976  kercvrlsm  31029  pwssplit4  31035  hbtlem5  31077  proot1hash  31160  radcnvrat  31195  nznngen  31221  refsumcn  31405  icoiccdif  31564  lptioo2  31637  lptioo1  31638  icccncfext  31690  stoweidlem27  31809  stoweidlem46  31828  stoweidlem57  31839  fourierdlem40  31929  fourierdlem78  31967  ffnafv  32256  elpwdifsn  32296  funcestrcsetclem8  32653  funcsetcestrclem8  32668  rnghmsscmap2  32781  rnghmsscmap  32782  funcrngcsetc  32806  funcrngcsetcALT  32807  rhmsscmap2  32827  rhmsscmap  32828  rhmsscrnghm  32834  rngcresringcat  32838  funcringcsetc  32843  funcringcsetcOLD2lem8  32851  funcringcsetclem8OLD  32874  rhmsubcOLDlem4  32916  ssnn0ssfz  32938  lincolss  33035  lcoss  33037  lcosslsp  33039  trsspwALT3  33618  sspwimpALT2  33728  bnj1033  34025  bnj1398  34090  lshpdisj  34712  lssats  34737  lkrlsp  34827  lkrin  34889  glbconxN  35102  paddss1  35541  paddss2  35542  paddasslem16  35559  paddidm  35565  pmodlem2  35571  pmapjoin  35576  pmapjat1  35577  pclfinN  35624  pclfinclN  35674  cdleme50rnlem  36270  diasslssN  36786  dia2dimlem12  36802  dihsslss  37003  baerlem3lem2  37437  baerlem5alem2  37438  baerlem5blem2  37439  hdmaprnN  37594  hgmaprnN  37631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator