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

Theorem ssrdv 3574
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 1842 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfss2 3557 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 223 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1473  wcel 1977  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  sscon  3706  ssdif  3707  unss1  3744  ssrin  3800  eq0rdv  3931  uniss  4389  intss1  4422  intmin  4427  intssuni  4429  iunss1  4463  iinss1  4464  ss2iun  4467  ssiun  4493  ssiun2  4494  iinss  4502  iinss2  4503  iunxdif3  4537  trintss  4692  sspwb  4838  pwssun  4934  relop  5182  dmss  5232  dmcosseq  5295  ssrnres  5477  sossfld  5485  predpo  5601  preddowncl  5610  tron  5649  tz7.7  5652  dffv2  6166  chfnrn  6221  fvn0ssdmfun  6243  fveqdmss  6247  dff3  6265  ffnfv  6280  f1imass  6400  ssorduni  6855  onint  6865  limsssuc  6920  limuni3  6922  limomss  6940  fo1stres  7061  fo2ndres  7062  fo2ndf  7149  fnse  7159  ressuppssdif  7181  suppss  7190  reldmtpos  7225  wfrlem10  7289  onfununi  7303  smoiun  7323  smorndom  7330  tz7.48-1  7403  tz7.49  7405  oaass  7506  qsss  7673  uniinqs  7692  pmss12g  7748  mapss  7764  ixpssmap2g  7801  ixpssmapg  7802  fineqv  8038  pssnn  8041  ssfii  8186  dffi2  8190  ordtypelem9  8292  ordtypelem10  8293  oismo  8306  unxpwdom2  8354  inf3lemd  8385  inf3lem1  8386  inf3lem6  8391  cantnflem3  8449  cantnf  8451  cnfcom3lem  8461  onssr1  8555  rankunb  8574  tcrank  8608  harcard  8665  carduni  8668  infxpenlem  8697  infpwfien  8746  dfac12r  8829  ackbij2lem1  8902  ackbij1lem18  8920  isfin1-3  9069  fin1a2lem11  9093  fin1a2lem13  9095  zorn2lem4  9182  zorn2lem5  9183  ttukeylem6  9197  ttukeylem7  9198  fpwwe2lem11  9319  fpwwe2lem12  9320  fpwwe2  9322  wunr1om  9398  wunom  9399  tskr1om  9446  tskr1om2  9447  tskxpss  9451  tskcard  9460  tskuni  9462  grothomex  9508  genpss  9683  distrlem1pr  9704  distrlem5pr  9706  prlem934  9712  ltexprlem2  9716  ltexprlem6  9720  ltexprlem7  9721  reclem3pr  9728  reclem4pr  9729  supaddc  10840  supadd  10841  supmul1  10842  supmullem2  10844  peano5uzi  11301  uzss  11543  ixxdisj  12020  ixxss1  12023  ixxss2  12024  ixxss12  12025  ixxub  12026  ixxlb  12027  iocssre  12083  icossre  12084  iccssre  12085  icodisj  12127  fzss1  12209  fzss2  12210  fzosplit  12328  fzouzsplit  12330  ssfzo12bi  12387  ssnn0fi  12604  fsuppmapnn0fiub  12610  fsuppmapnn0fiubOLD  12611  suppssfz  12614  sswrd  13117  rtrclreclem3  13597  isercoll  14195  summolem2a  14242  fsumcvg3  14256  fsum2dlem  14292  fsumcom2  14296  fsumcom2OLD  14297  qshash  14347  prodmolem2a  14452  fprod2dlem  14498  fprodcom2  14502  fprodcom2OLD  14503  bitsfzo  14944  phimullem  15271  prmreclem5  15411  1arith  15418  vdwlem2  15473  vdwlem6  15477  vdwlem8  15479  ramtlecl  15491  prmgaplem3  15544  prmgaplem4  15545  monhom  16167  epihom  16174  funcsetcres2  16515  funcestrcsetclem8  16559  funcsetcestrclem8  16574  psdmrn  16979  psssdm2  16987  gsumwspan  17155  frmdss2  17172  ssnmz  17408  conjnmz  17466  gex1  17778  sylow2alem1  17804  sylow3lem3  17816  lsmless1x  17831  lsmless2x  17832  lsmub1x  17833  lsmub2x  17834  lsmmod  17860  lsmdisj2  17867  efgrelexlemb  17935  efgcpbllemb  17940  cntzcmn  18017  gsum2d2  18145  dprdub  18196  dprdss  18200  dprddisj2  18210  ablfacrp  18237  pgpfac1lem3  18248  kerf1hrm  18515  isdrng2  18529  subrguss  18567  subrgmre  18576  lssssr  18723  lsssssubg  18728  lssmre  18736  lbspss  18852  lspdisj  18895  lbsextlem2  18929  lidl1el  18988  drngnidl  18999  lpiss  19020  unitrrg  19063  fidomndrng  19077  mplbas2  19240  zsssubrg  19572  qsssubdrg  19573  cnsubrg  19574  mulgrhm2  19614  znrrg  19681  ocvocv  19782  ocv2ss  19784  ocvin  19785  lsmcss  19803  cssmre  19804  pjfo  19826  pjcss  19827  obs2ss  19840  frlmsslsp  19902  lindfrn  19927  dmatsgrp  20072  scmatsgrp  20092  scmatsgrp1  20095  m2cpmrngiso  20330  bastg  20529  tgss  20531  tgtop  20536  tgidm  20543  en2top  20548  neisspw  20669  topssnei  20686  neiptopuni  20692  lpss3  20706  clslp  20710  tgrest  20721  ssrest  20738  restfpw  20741  restntr  20744  ordtbas2  20753  ordtbas  20754  cnss1  20838  cnss2  20839  cnsscnp  20841  cnrest2r  20849  cmpsublem  20960  cmpsub  20961  tgcmp  20962  cmpcld  20963  hauscmplem  20967  cnconn  20983  2ndcsep  21020  llyss  21040  nllyss  21041  restnlly  21043  restlly  21044  locfincmp  21087  locfincf  21092  kgenss  21104  kgenidm  21108  llycmpkgen2  21111  1stckgen  21115  kgen2ss  21116  kgencn3  21119  ptbasfi  21142  ptpjopn  21173  ptclsg  21176  txdis  21193  txkgen  21213  xkoptsub  21215  xkopjcn  21217  txcon  21250  qtoptop2  21260  qtopuni  21263  qtopkgen  21271  basqtop  21272  tgqtop  21273  qtopss  21276  qtoprest  21278  qtopomap  21279  qtopcmap  21280  kqsat  21292  kqcldsat  21294  hmphdis  21357  isfild  21420  ssfg  21434  fgss  21435  fgss2  21436  fgfil  21437  fgabs  21441  filcon  21445  fgtr  21452  trfg  21453  uzrest  21459  ufilmax  21469  ufileu  21481  filufint  21482  rnelfm  21515  fmfnfmlem2  21517  fmfnfmlem4  21519  flimss2  21534  flimss1  21535  flimclsi  21540  flimcf  21544  flimsncls  21548  fclssscls  21580  fclsss1  21584  fclsss2  21585  fclscf  21587  uffclsflim  21593  alexsublem  21606  alexsubALTlem3  21611  ptcmplem2  21615  ptcmplem3  21616  cnextf  21628  symgtgp  21663  cldsubg  21672  tsmscl  21696  haustsms2  21698  tgptsmscls  21711  tsmsxp  21716  restutop  21799  restutopopn  21800  ustuqtop4  21806  utop2nei  21812  utop3cls  21813  ucncn  21847  xblss2ps  21964  xblss2  21965  unirnblps  21982  unirnbl  21983  xrsblre  22370  xrsmopn  22371  recld2  22373  zdis  22375  icccmplem2  22382  cncfss  22458  cnheiborlem  22509  htpycn  22528  phtpyhtpy  22537  pi1blem  22595  clsocv  22802  cfilfcls  22825  iscmet3lem2  22843  iscmet2  22845  caussi  22848  equivcfil  22850  lmcau  22864  cmetss  22866  pjth  22963  hlhil  22967  ivthicc  22979  ovoliunnul  23027  ovolicopnf  23044  uniioombllem3  23104  dyadmbllem  23118  opnmbllem  23120  volsup2  23124  vitalilem2  23129  itg1addlem4  23217  itg10a  23228  itg1ge0a  23229  mbfi1fseqlem4  23236  itg2gt0  23278  limciun  23409  perfdvf  23418  dvidlem  23430  cpnord  23449  dvaddf  23456  dvmulf  23457  dvcof  23462  dvcj  23464  dvrec  23469  dvcnv  23489  dvlip2  23507  dvivth  23522  dvne0  23523  dvcnvre  23531  ftc1cn  23555  ply1lpir  23687  plyco0  23697  plyexmo  23817  ulmdv  23906  pserdv  23932  abelth  23944  efif1o  24041  logno1  24127  efopnlem2  24148  loglesqrt  24244  lgamcvg2  24526  ppisval  24575  ppisval2  24576  ppinprm  24623  chtnprm  24625  fsumvma  24683  dchrfi  24725  chtppilimlem2  24908  chebbnd2  24911  vmadivsumb  24917  rplogsumlem2  24919  dchrisumlem2  24924  vmalogdivsum2  24972  vmalogdivsum  24973  2vmadivsumlem  24974  selbergb  24983  selberg2b  24986  selberg3lem1  24991  selberg3lem2  24992  selberg3  24993  selberg4lem1  24994  selberg4  24995  pntrlog2bndlem2  25012  pntrlog2bndlem4  25014  sizeusglecusglem1  25806  clwwlkssclwwlkn  26114  ococss  27330  shsub1  27361  shless  27396  shmodsi  27426  pjhth  27430  spansnss  27608  spanpr  27617  spansnm0i  27687  pjjsi  27737  sumdmdii  28452  sumdmdlem  28455  sumdmdlem2  28456  cdj3lem1  28471  abrexss  28528  rnmpt2ss  28650  unifi3  28667  ssnnssfz  28731  reff  29028  crefss  29038  cmpcref  29039  tpr2rico  29080  esumrnmpt2  29251  esumpcvgval  29261  ldsysgenld  29344  sigapildsys  29346  ldgenpisys  29350  cldssbrsiga  29371  measdivcstOLD  29408  mbfmcnt  29451  dya2iocuni  29466  oddpwdc  29537  eulerpartlemgs2  29563  bnj1033  30085  bnj1398  30150  sconpi1  30269  cvmscld  30303  cvmsss2  30304  cvmliftlem15  30328  dfon2lem6  30731  nofulllem5  30899  fnessref  31316  fgmin  31329  tailfb  31336  dissneqlem  32157  icoreresf  32170  finxpreclem6  32203  lindsenlbs  32368  poimirlem11  32384  poimirlem12  32385  opnmbllem0  32409  ftc1cnnc  32448  sstotbnd3  32539  prdstotbnd  32557  cntotbnd  32559  ismtyhmeo  32568  1idl  32789  lshpdisj  33086  lssats  33111  lkrlsp  33201  lkrin  33263  glbconxN  33476  paddss1  33915  paddss2  33916  paddasslem16  33933  paddidm  33939  pmodlem2  33945  pmapjoin  33950  pmapjat1  33951  pclfinN  33998  pclfinclN  34048  cdleme50rnlem  34644  diasslssN  35160  dia2dimlem12  35176  dihsslss  35377  baerlem3lem2  35811  baerlem5alem2  35812  baerlem5blem2  35813  hdmaprnN  35968  hgmaprnN  36005  eldiophss  36150  rencldnfilem  36196  pellexlem5  36209  pell14qrss1234  36232  pell1qrss14  36244  pellfundre  36257  pellfundge  36258  pellfundlb  36260  pellfundglb  36261  harinf  36413  kercvrlsm  36465  pwssplit4  36471  hbtlem5  36511  proot1hash  36591  intabssd  36729  ss2iundf  36764  ov2ssiunov2  36805  clsk1indlem3  37155  radcnvrat  37329  nznngen  37331  trsspwALT3  37863  sspwimpALT2  37980  refsumcn  38006  icoiccdif  38391  lptioo2  38492  lptioo1  38493  icccncfext  38567  stoweidlem27  38714  stoweidlem46  38733  stoweidlem57  38744  fourierdlem40  38834  fourierdlem78  38871  ffnafv  39695  iccpartrn  39763  elpwdifsn  40107  uhgredgss  40356  usgruspgrb  40403  uhgrissubgr  40491  uhgrspansubgrlem  40506  uhgrspan1  40519  nbgrssvtx  40574  nbgrssovtx  40578  cusgredg  40638  usgredgsscusgredg  40667  rnghmsscmap2  41757  rnghmsscmap  41758  funcrngcsetc  41782  funcrngcsetcALT  41783  rhmsscmap2  41803  rhmsscmap  41804  rhmsscrnghm  41810  rngcresringcat  41814  funcringcsetc  41819  funcringcsetcALTV2lem8  41827  funcringcsetclem8ALTV  41850  rhmsubcALTVlem4  41892  ssnn0ssfz  41912  lincolss  42009  lcoss  42011  lcosslsp  42013
  Copyright terms: Public domain W3C validator