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  4394  intss1  4427  intmin  4432  intssuni  4434  iunss1  4468  iinss1  4469  ss2iun  4472  ssiun  4498  ssiun2  4499  iinss  4507  iinss2  4508  iunxdif3  4542  trintss  4697  sspwb  4844  pwssun  4944  relop  5194  dmss  5245  dmcosseq  5308  ssrnres  5491  sossfld  5499  predpo  5615  preddowncl  5624  tron  5663  tz7.7  5666  dffv2  6181  chfnrn  6236  fvn0ssdmfun  6258  fveqdmss  6262  dff3  6280  ffnfv  6295  f1imass  6422  ssorduni  6877  onint  6887  limsssuc  6942  limuni3  6944  limomss  6962  fo1stres  7083  fo2ndres  7084  fo2ndf  7171  fnse  7181  ressuppssdif  7203  suppss  7212  reldmtpos  7247  wfrlem10  7311  onfununi  7325  smoiun  7345  smorndom  7352  tz7.48-1  7425  tz7.49  7427  oaass  7528  qsss  7695  uniinqs  7714  pmss12g  7770  mapss  7786  ixpssmap2g  7823  ixpssmapg  7824  fineqv  8060  pssnn  8063  ssfii  8208  dffi2  8212  ordtypelem9  8314  ordtypelem10  8315  oismo  8328  unxpwdom2  8376  inf3lemd  8407  inf3lem1  8408  inf3lem6  8413  cantnflem3  8471  cantnf  8473  cnfcom3lem  8483  onssr1  8577  rankunb  8596  tcrank  8630  harcard  8687  carduni  8690  infxpenlem  8719  infpwfien  8768  dfac12r  8851  ackbij2lem1  8924  ackbij1lem18  8942  isfin1-3  9091  fin1a2lem11  9115  fin1a2lem13  9117  zorn2lem4  9204  zorn2lem5  9205  ttukeylem6  9219  ttukeylem7  9220  fpwwe2lem11  9341  fpwwe2lem12  9342  fpwwe2  9344  wunr1om  9420  wunom  9421  tskr1om  9468  tskr1om2  9469  tskxpss  9473  tskcard  9482  tskuni  9484  grothomex  9530  genpss  9705  distrlem1pr  9726  distrlem5pr  9728  prlem934  9734  ltexprlem2  9738  ltexprlem6  9742  ltexprlem7  9743  reclem3pr  9750  reclem4pr  9751  supaddc  10867  supadd  10868  supmul1  10869  supmullem2  10871  peano5uzi  11342  uzss  11584  ixxdisj  12061  ixxss1  12064  ixxss2  12065  ixxss12  12066  ixxub  12067  ixxlb  12068  iocssre  12124  icossre  12125  iccssre  12126  icodisj  12168  fzss1  12251  fzss2  12252  fzosplit  12370  fzouzsplit  12372  ssfzo12bi  12429  ssnn0fi  12646  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  suppssfz  12656  sswrd  13168  rtrclreclem3  13648  isercoll  14246  summolem2a  14293  fsumcvg3  14307  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  qshash  14398  prodmolem2a  14503  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  bitsfzo  14995  phimullem  15322  prmreclem5  15462  1arith  15469  vdwlem2  15524  vdwlem6  15528  vdwlem8  15530  ramtlecl  15542  prmgaplem3  15595  prmgaplem4  15596  monhom  16218  epihom  16225  funcsetcres2  16566  funcestrcsetclem8  16610  funcsetcestrclem8  16625  psdmrn  17030  psssdm2  17038  gsumwspan  17206  frmdss2  17223  ssnmz  17459  conjnmz  17517  gex1  17829  sylow2alem1  17855  sylow3lem3  17867  lsmless1x  17882  lsmless2x  17883  lsmub1x  17884  lsmub2x  17885  lsmmod  17911  lsmdisj2  17918  efgrelexlemb  17986  efgcpbllemb  17991  cntzcmn  18068  gsum2d2  18196  dprdub  18247  dprdss  18251  dprddisj2  18261  ablfacrp  18288  pgpfac1lem3  18299  kerf1hrm  18566  isdrng2  18580  subrguss  18618  subrgmre  18627  lssssr  18774  lsssssubg  18779  lssmre  18787  lbspss  18903  lspdisj  18946  lbsextlem2  18980  lidl1el  19039  drngnidl  19050  lpiss  19071  unitrrg  19114  fidomndrng  19128  mplbas2  19291  zsssubrg  19623  qsssubdrg  19624  cnsubrg  19625  mulgrhm2  19666  znrrg  19733  ocvocv  19834  ocv2ss  19836  ocvin  19837  lsmcss  19855  cssmre  19856  pjfo  19878  pjcss  19879  obs2ss  19892  frlmsslsp  19954  lindfrn  19979  dmatsgrp  20124  scmatsgrp  20144  scmatsgrp1  20147  m2cpmrngiso  20382  bastg  20581  tgss  20583  tgtop  20588  tgidm  20595  en2top  20600  neisspw  20721  topssnei  20738  neiptopuni  20744  lpss3  20758  clslp  20762  tgrest  20773  ssrest  20790  restfpw  20793  restntr  20796  ordtbas2  20805  ordtbas  20806  cnss1  20890  cnss2  20891  cnsscnp  20893  cnrest2r  20901  cmpsublem  21012  cmpsub  21013  tgcmp  21014  cmpcld  21015  hauscmplem  21019  cnconn  21035  2ndcsep  21072  llyss  21092  nllyss  21093  restnlly  21095  restlly  21096  locfincmp  21139  locfincf  21144  kgenss  21156  kgenidm  21160  llycmpkgen2  21163  1stckgen  21167  kgen2ss  21168  kgencn3  21171  ptbasfi  21194  ptpjopn  21225  ptclsg  21228  txdis  21245  txkgen  21265  xkoptsub  21267  xkopjcn  21269  txcon  21302  qtoptop2  21312  qtopuni  21315  qtopkgen  21323  basqtop  21324  tgqtop  21325  qtopss  21328  qtoprest  21330  qtopomap  21331  qtopcmap  21332  kqsat  21344  kqcldsat  21346  hmphdis  21409  isfild  21472  ssfg  21486  fgss  21487  fgss2  21488  fgfil  21489  fgabs  21493  filcon  21497  fgtr  21504  trfg  21505  uzrest  21511  ufilmax  21521  ufileu  21533  filufint  21534  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem4  21571  flimss2  21586  flimss1  21587  flimclsi  21592  flimcf  21596  flimsncls  21600  fclssscls  21632  fclsss1  21636  fclsss2  21637  fclscf  21639  uffclsflim  21645  alexsublem  21658  alexsubALTlem3  21663  ptcmplem2  21667  ptcmplem3  21668  cnextf  21680  symgtgp  21715  cldsubg  21724  tsmscl  21748  haustsms2  21750  tgptsmscls  21763  tsmsxp  21768  restutop  21851  restutopopn  21852  ustuqtop4  21858  utop2nei  21864  utop3cls  21865  ucncn  21899  xblss2ps  22016  xblss2  22017  unirnblps  22034  unirnbl  22035  xrsblre  22422  xrsmopn  22423  recld2  22425  zdis  22427  icccmplem2  22434  cncfss  22510  cnheiborlem  22561  htpycn  22580  phtpyhtpy  22589  pi1blem  22647  clsocv  22857  cfilfcls  22880  iscmet3lem2  22898  iscmet2  22900  caussi  22903  equivcfil  22905  lmcau  22919  cmetss  22921  pjth  23018  hlhil  23022  ivthicc  23034  ovoliunnul  23082  ovolicopnf  23099  uniioombllem3  23159  dyadmbllem  23173  opnmbllem  23175  volsup2  23179  vitalilem2  23184  itg1addlem4  23272  itg10a  23283  itg1ge0a  23284  mbfi1fseqlem4  23291  itg2gt0  23333  limciun  23464  perfdvf  23473  dvidlem  23485  cpnord  23504  dvaddf  23511  dvmulf  23512  dvcof  23517  dvcj  23519  dvrec  23524  dvcnv  23544  dvlip2  23562  dvivth  23577  dvne0  23578  dvcnvre  23586  ftc1cn  23610  ply1lpir  23742  plyco0  23752  plyexmo  23872  ulmdv  23961  pserdv  23987  abelth  23999  efif1o  24096  logno1  24182  efopnlem2  24203  loglesqrt  24299  lgamcvg2  24581  ppisval  24630  ppisval2  24631  ppinprm  24678  chtnprm  24680  fsumvma  24738  dchrfi  24780  chtppilimlem2  24963  chebbnd2  24966  vmadivsumb  24972  rplogsumlem2  24974  dchrisumlem2  24979  vmalogdivsum2  25027  vmalogdivsum  25028  2vmadivsumlem  25029  selbergb  25038  selberg2b  25041  selberg3lem1  25046  selberg3lem2  25047  selberg3  25048  selberg4lem1  25049  selberg4  25050  pntrlog2bndlem2  25067  pntrlog2bndlem4  25069  uhgredgss  25805  sizeusglecusglem1  26012  clwwlkssclwwlkn  26320  ococss  27536  shsub1  27567  shless  27602  shmodsi  27632  pjhth  27636  spansnss  27814  spanpr  27823  spansnm0i  27893  pjjsi  27943  sumdmdii  28658  sumdmdlem  28661  sumdmdlem2  28662  cdj3lem1  28677  abrexss  28734  rnmpt2ss  28856  unifi3  28873  ssnnssfz  28937  reff  29234  crefss  29244  cmpcref  29245  tpr2rico  29286  esumrnmpt2  29457  esumpcvgval  29467  ldsysgenld  29550  sigapildsys  29552  ldgenpisys  29556  cldssbrsiga  29577  measdivcstOLD  29614  mbfmcnt  29657  dya2iocuni  29672  oddpwdc  29743  eulerpartlemgs2  29769  bnj1033  30291  bnj1398  30356  sconpi1  30475  cvmscld  30509  cvmsss2  30510  cvmliftlem15  30534  dfon2lem6  30937  nofulllem5  31105  fnessref  31522  fgmin  31535  tailfb  31542  dissneqlem  32363  icoreresf  32376  finxpreclem6  32409  lindsenlbs  32574  poimirlem11  32590  poimirlem12  32591  opnmbllem0  32615  ftc1cnnc  32654  sstotbnd3  32745  prdstotbnd  32763  cntotbnd  32765  ismtyhmeo  32774  1idl  32995  lshpdisj  33292  lssats  33317  lkrlsp  33407  lkrin  33469  glbconxN  33682  paddss1  34121  paddss2  34122  paddasslem16  34139  paddidm  34145  pmodlem2  34151  pmapjoin  34156  pmapjat1  34157  pclfinN  34204  pclfinclN  34254  cdleme50rnlem  34850  diasslssN  35366  dia2dimlem12  35382  dihsslss  35583  baerlem3lem2  36017  baerlem5alem2  36018  baerlem5blem2  36019  hdmaprnN  36174  hgmaprnN  36211  eldiophss  36356  rencldnfilem  36402  pellexlem5  36415  pell14qrss1234  36438  pell1qrss14  36450  pellfundre  36463  pellfundge  36464  pellfundlb  36466  pellfundglb  36467  harinf  36619  kercvrlsm  36671  pwssplit4  36677  hbtlem5  36717  proot1hash  36797  intabssd  36935  ss2iundf  36970  ov2ssiunov2  37011  clsk1indlem3  37361  radcnvrat  37535  nznngen  37537  trsspwALT3  38069  sspwimpALT2  38186  refsumcn  38212  icoiccdif  38597  lptioo2  38698  lptioo1  38699  icccncfext  38773  stoweidlem27  38920  stoweidlem46  38939  stoweidlem57  38950  fourierdlem40  39040  fourierdlem78  39077  ffnafv  39900  iccpartrn  39968  elpwdifsn  40312  usgruspgrb  40411  uhgrissubgr  40499  uhgrspansubgrlem  40514  uhgrspan1  40527  nbgrssvtx  40582  nbgrssovtx  40586  cusgredg  40646  usgredgsscusgredg  40675  rnghmsscmap2  41765  rnghmsscmap  41766  funcrngcsetc  41790  funcrngcsetcALT  41791  rhmsscmap2  41811  rhmsscmap  41812  rhmsscrnghm  41818  rngcresringcat  41822  funcringcsetc  41827  funcringcsetcALTV2lem8  41835  funcringcsetclem8ALTV  41858  rhmsubcALTVlem4  41900  ssnn0ssfz  41920  lincolss  42017  lcoss  42019  lcosslsp  42021  iunord  42220
  Copyright terms: Public domain W3C validator