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

Theorem ssrdv 3642
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 1895 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfss2 3624 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 224 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1521  wcel 2030  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  sscon  3777  ssdif  3778  unss1  3815  ssrin  3871  eq0rdv  4012  elpwdifsn  4352  uniss  4490  intss1  4524  intmin  4529  intssuni  4531  iunss1  4564  iinss1  4565  ss2iun  4568  ssiun  4594  ssiun2  4595  iinss  4603  iinss2  4604  iunxdif3  4638  trintssOLD  4803  sspwb  4947  pwssun  5049  relop  5305  dmss  5355  dmcosseq  5419  ssrnres  5607  sossfld  5615  predpo  5736  preddowncl  5745  tron  5784  tz7.7  5787  dffv2  6310  chfnrn  6368  fvn0ssdmfun  6390  fveqdmss  6394  dff3  6412  ffnfv  6428  f1imass  6561  ssorduni  7027  onint  7037  limsssuc  7092  limuni3  7094  limomss  7112  fo1stres  7236  fo2ndres  7237  fo2ndf  7329  fnse  7339  ressuppssdif  7361  suppss  7370  reldmtpos  7405  wfrlem10  7469  onfununi  7483  smoiun  7503  smorndom  7510  tz7.48-1  7583  tz7.49  7585  oaass  7686  qsss  7851  uniinqs  7870  pmss12g  7926  mapss  7942  ixpssmap2g  7979  ixpssmapg  7980  fineqv  8216  pssnn  8219  ssfii  8366  dffi2  8370  ordtypelem9  8472  ordtypelem10  8473  oismo  8486  unxpwdom2  8534  inf3lemd  8562  inf3lem1  8563  inf3lem6  8568  cantnflem3  8626  cantnf  8628  cnfcom3lem  8638  onssr1  8732  rankunb  8751  tcrank  8785  harcard  8842  carduni  8845  infxpenlem  8874  infpwfien  8923  dfac12r  9006  ackbij2lem1  9079  ackbij1lem18  9097  isfin1-3  9246  fin1a2lem11  9270  fin1a2lem13  9272  zorn2lem4  9359  zorn2lem5  9360  ttukeylem6  9374  ttukeylem7  9375  fpwwe2lem11  9500  fpwwe2lem12  9501  fpwwe2  9503  wunr1om  9579  wunom  9580  tskr1om  9627  tskr1om2  9628  tskxpss  9632  tskcard  9641  tskuni  9643  grothomex  9689  genpss  9864  distrlem1pr  9885  distrlem5pr  9887  prlem934  9893  ltexprlem2  9897  ltexprlem6  9901  ltexprlem7  9902  reclem3pr  9909  reclem4pr  9910  supaddc  11028  supadd  11029  supmul1  11030  supmullem2  11032  peano5uzi  11504  uzss  11746  ixxdisj  12228  ixxss1  12231  ixxss2  12232  ixxss12  12233  ixxub  12234  ixxlb  12235  iocssre  12291  icossre  12292  iccssre  12293  icodisj  12335  fzss1  12418  fzss2  12419  ssfzunsnext  12424  fzosplit  12540  fzouzsplit  12542  ssfzo12bi  12603  ssnn0fi  12824  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  suppssfz  12834  sswrd  13345  rtrclreclem3  13844  isercoll  14442  summolem2a  14490  fsumcvg3  14504  fsum2dlem  14545  fsumcom2  14549  fsumcom2OLD  14550  qshash  14603  prodmolem2a  14708  fprod2dlem  14754  fprodcom2  14758  fprodcom2OLD  14759  bitsfzo  15204  phimullem  15531  prmreclem5  15671  1arith  15678  vdwlem2  15733  vdwlem6  15737  vdwlem8  15739  ramtlecl  15751  prmgaplem3  15804  prmgaplem4  15805  monhom  16442  epihom  16449  funcsetcres2  16790  funcestrcsetclem8  16834  funcsetcestrclem8  16849  psdmrn  17254  psssdm2  17262  gsumwspan  17430  frmdss2  17447  ssnmz  17683  conjnmz  17741  gex1  18052  sylow2alem1  18078  sylow3lem3  18090  lsmless1x  18105  lsmless2x  18106  lsmub1x  18107  lsmub2x  18108  lsmmod  18134  lsmdisj2  18141  efgrelexlemb  18209  efgcpbllemb  18214  cntzcmn  18291  gsum2d2  18419  dprdub  18470  dprdss  18474  dprddisj2  18484  ablfacrp  18511  pgpfac1lem3  18522  kerf1hrm  18791  isdrng2  18805  subrguss  18843  subrgmre  18852  lssssr  19001  lsssssubg  19006  lssmre  19014  lbspss  19130  lspdisj  19173  lbsextlem2  19207  lidl1el  19266  drngnidl  19277  lpiss  19298  unitrrg  19341  fidomndrng  19355  mplbas2  19518  zsssubrg  19852  qsssubdrg  19853  cnsubrg  19854  mulgrhm2  19895  znrrg  19962  ocvocv  20063  ocv2ss  20065  ocvin  20066  lsmcss  20084  cssmre  20085  pjfo  20107  pjcss  20108  obs2ss  20121  frlmsslsp  20183  lindfrn  20208  dmatsgrp  20353  scmatsgrp  20373  scmatsgrp1  20376  m2cpmrngiso  20611  bastg  20818  tgss  20820  tgtop  20825  tgidm  20832  en2top  20837  neisspw  20959  topssnei  20976  neiptopuni  20982  lpss3  20996  clslp  21000  tgrest  21011  ssrest  21028  restfpw  21031  restntr  21034  ordtbas2  21043  ordtbas  21044  cnss1  21128  cnss2  21129  cnsscnp  21131  cnrest2r  21139  cmpsublem  21250  cmpsub  21251  tgcmp  21252  cmpcld  21253  hauscmplem  21257  cnconn  21273  2ndcsep  21310  llyss  21330  nllyss  21331  restnlly  21333  restlly  21334  locfincmp  21377  locfincf  21382  kgenss  21394  kgenidm  21398  llycmpkgen2  21401  1stckgen  21405  kgen2ss  21406  kgencn3  21409  ptbasfi  21432  ptpjopn  21463  ptclsg  21466  txdis  21483  txkgen  21503  xkoptsub  21505  xkopjcn  21507  txconn  21540  qtoptop2  21550  qtopuni  21553  qtopkgen  21561  basqtop  21562  tgqtop  21563  qtopss  21566  qtoprest  21568  qtopomap  21569  qtopcmap  21570  kqsat  21582  kqcldsat  21584  hmphdis  21647  isfild  21709  ssfg  21723  fgss  21724  fgss2  21725  fgfil  21726  fgabs  21730  filconn  21734  fgtr  21741  trfg  21742  uzrest  21748  ufilmax  21758  ufileu  21770  filufint  21771  rnelfm  21804  fmfnfmlem2  21806  fmfnfmlem4  21808  flimss2  21823  flimss1  21824  flimclsi  21829  flimcf  21833  flimsncls  21837  fclssscls  21869  fclsss1  21873  fclsss2  21874  fclscf  21876  uffclsflim  21882  alexsublem  21895  alexsubALTlem3  21900  ptcmplem2  21904  ptcmplem3  21905  cnextf  21917  symgtgp  21952  cldsubg  21961  tsmscl  21985  haustsms2  21987  tgptsmscls  22000  tsmsxp  22005  restutop  22088  restutopopn  22089  ustuqtop4  22095  utop2nei  22101  utop3cls  22102  ucncn  22136  xblss2ps  22253  xblss2  22254  unirnblps  22271  unirnbl  22272  xrsblre  22661  xrsmopn  22662  recld2  22664  zdis  22666  icccmplem2  22673  cncfss  22749  cnheiborlem  22800  htpycn  22819  phtpyhtpy  22828  pi1blem  22885  clsocv  23095  cfilfcls  23118  iscmet3lem2  23136  iscmet2  23138  caussi  23141  equivcfil  23143  lmcau  23157  cmetss  23159  pjth  23256  hlhil  23260  ivthicc  23273  ovoliunnul  23321  ovolicopnf  23338  uniioombllem3  23399  dyadmbllem  23413  opnmbllem  23415  volsup2  23419  vitalilem2  23423  itg1addlem4  23511  itg10a  23522  itg1ge0a  23523  mbfi1fseqlem4  23530  itg2gt0  23572  limciun  23703  perfdvf  23712  dvidlem  23724  cpnord  23743  dvaddf  23750  dvmulf  23751  dvcof  23756  dvcj  23758  dvrec  23763  dvcnv  23785  dvlip2  23803  dvivth  23818  dvne0  23819  dvcnvre  23827  ftc1cn  23851  ply1lpir  23983  plyco0  23993  plyexmo  24113  ulmdv  24202  pserdv  24228  abelth  24240  efif1o  24337  logno1  24427  efopnlem2  24448  loglesqrt  24544  lgamcvg2  24826  ppisval  24875  ppisval2  24876  ppinprm  24923  chtnprm  24925  fsumvma  24983  dchrfi  25025  chtppilimlem2  25208  chebbnd2  25211  vmadivsumb  25217  rplogsumlem2  25219  dchrisumlem2  25224  vmalogdivsum2  25272  vmalogdivsum  25273  2vmadivsumlem  25274  selbergb  25283  selberg2b  25286  selberg3lem1  25291  selberg3lem2  25292  selberg3  25293  selberg4lem1  25294  selberg4  25295  pntrlog2bndlem2  25312  pntrlog2bndlem4  25314  uhgredgss  26071  usgruspgrb  26121  uhgrissubgr  26212  uhgrspansubgrlem  26227  uhgrspan1  26240  nbgrssvtxOLD  26283  nbgrssovtxOLD  26305  cusgredg  26376  usgredgsscusgredg  26411  ococss  28280  shsub1  28311  shless  28346  shmodsi  28376  pjhth  28380  spansnss  28558  spanpr  28567  spansnm0i  28637  pjjsi  28687  sumdmdii  29402  sumdmdlem  29405  sumdmdlem2  29406  cdj3lem1  29421  abrexss  29476  iinssiun  29503  rnmpt2ss  29601  unifi3  29618  uzssico  29674  ssnnssfz  29677  reff  30034  crefss  30044  cmpcref  30045  tpr2rico  30086  esumrnmpt2  30258  esumpcvgval  30268  ldsysgenld  30351  sigapildsys  30353  ldgenpisys  30357  cldssbrsiga  30378  measdivcstOLD  30415  mbfmcnt  30458  dya2iocuni  30473  oddpwdc  30544  eulerpartlemgs2  30570  reprpmtf1o  30832  bnj1033  31163  bnj1398  31228  sconnpi1  31347  cvmscld  31381  cvmsss2  31382  cvmliftlem15  31406  dfon2lem6  31817  fnessref  32477  fgmin  32490  tailfb  32497  dissneqlem  33317  icoreresf  33330  finxpreclem6  33363  lindsenlbs  33534  poimirlem11  33550  poimirlem12  33551  opnmbllem0  33575  ftc1cnnc  33614  sstotbnd3  33705  prdstotbnd  33723  cntotbnd  33725  ismtyhmeo  33734  1idl  33955  lshpdisj  34592  lssats  34617  lkrlsp  34707  lkrin  34769  glbconxN  34982  paddss1  35421  paddss2  35422  paddasslem16  35439  paddidm  35445  pmodlem2  35451  pmapjoin  35456  pmapjat1  35457  pclfinN  35504  pclfinclN  35554  cdleme50rnlem  36149  diasslssN  36665  dia2dimlem12  36681  dihsslss  36882  baerlem3lem2  37316  baerlem5alem2  37317  baerlem5blem2  37318  hdmaprnN  37473  hgmaprnN  37510  eldiophss  37655  rencldnfilem  37701  pellexlem5  37714  pell14qrss1234  37737  pell1qrss14  37749  pellfundre  37762  pellfundge  37763  pellfundlb  37765  pellfundglb  37766  harinf  37918  kercvrlsm  37970  pwssplit4  37976  hbtlem5  38015  proot1hash  38095  intabssd  38233  ss2iundf  38268  ov2ssiunov2  38309  clsk1indlem3  38658  radcnvrat  38830  nznngen  38832  trsspwALT3  39364  sspwimpALT2  39478  refsumcn  39503  iinssf  39641  icoiccdif  40068  lptioo2  40181  lptioo1  40182  icccncfext  40418  stoweidlem27  40562  stoweidlem46  40581  stoweidlem57  40592  fourierdlem40  40682  fourierdlem78  40719  ffnafv  41572  iccpartrn  41691  sprsymrelfvlem  42065  sprsymrelf1lem  42066  rnghmsscmap2  42298  rnghmsscmap  42299  funcrngcsetc  42323  funcrngcsetcALT  42324  rhmsscmap2  42344  rhmsscmap  42345  rhmsscrnghm  42351  rngcresringcat  42355  funcringcsetc  42360  funcringcsetcALTV2lem8  42368  funcringcsetclem8ALTV  42391  rhmsubcALTVlem4  42432  ssnn0ssfz  42452  lincolss  42548  lcoss  42550  lcosslsp  42552  iunord  42747
  Copyright terms: Public domain W3C validator