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

Theorem ssrdv 3959
Description: Deduction 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 1929 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfss2 3939 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 237 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1536  wcel 2115  wss 3919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-in 3926  df-ss 3936
This theorem is referenced by:  eqelssd  3974  sscon  4101  ssdif  4102  unss1  4141  ssrin  4195  eq0rdv  4340  sspw  4535  elpwdifsn  4706  uniss  4832  intss1  4877  intmin  4882  intssuni  4884  iinssiun  4918  iunss1  4919  iinss1  4920  ss2iun  4923  ssiun  4956  ssiun2  4957  iinss  4966  iinss2  4967  iunxdif3  5003  sspwb  5329  pwssun  5443  relop  5708  dmss  5758  dmcosseq  5831  ssrnres  6022  sossfld  6030  predpo  6153  preddowncl  6162  tron  6201  tz7.7  6204  dffv2  6747  chfnrn  6810  fvn0ssdmfun  6833  fveqdmss  6837  dff3  6857  ffnfv  6873  f1imass  7014  ssorduni  7494  onint  7504  limsssuc  7559  limuni3  7561  limomss  7579  fo1stres  7710  fo2ndres  7711  fo2ndf  7813  fnse  7823  ressuppssdif  7847  suppss  7856  reldmtpos  7896  onfununi  7974  smoiun  7994  smorndom  8001  tz7.48-1  8075  tz7.49  8077  oaass  8183  qsss  8354  uniinqs  8373  pmss12g  8429  mapss  8449  ixpssmap2g  8487  ixpssmapg  8488  fineqv  8730  pssnn  8733  ssfii  8880  dffi2  8884  oismo  9001  unxpwdom2  9049  inf3lemd  9087  inf3lem1  9088  inf3lem6  9093  cantnflem3  9151  cantnf  9153  cnfcom3lem  9163  onssr1  9257  rankunb  9276  tcrank  9310  harcard  9404  carduni  9407  infxpenlem  9437  infpwfien  9486  dfac12r  9570  ackbij2lem1  9639  ackbij1lem18  9657  isfin1-3  9806  fin1a2lem11  9830  fin1a2lem13  9832  zorn2lem4  9919  zorn2lem5  9920  ttukeylem6  9934  ttukeylem7  9935  fpwwe2lem11  10060  fpwwe2lem12  10061  fpwwe2  10063  wunr1om  10139  wunom  10140  tskr1om  10187  tskr1om2  10188  tskxpss  10192  tskcard  10201  tskuni  10203  grothomex  10249  genpss  10424  distrlem1pr  10445  distrlem5pr  10447  ltexprlem2  10457  ltexprlem6  10461  ltexprlem7  10462  reclem3pr  10469  reclem4pr  10470  supaddc  11604  supadd  11605  supmul1  11606  supmullem2  11608  peano5uzi  12068  uzss  12262  ixxdisj  12750  ixxss1  12753  ixxss2  12754  ixxss12  12755  ixxub  12756  ixxlb  12757  iocssre  12814  icossre  12815  iccssre  12816  icodisj  12863  fzss1  12950  fzss2  12951  ssfzunsnext  12956  fzosplit  13074  fzouzsplit  13076  ssfzo12bi  13136  ssnn0fi  13357  fsuppmapnn0fiub  13363  suppssfz  13366  sswrd  13874  rtrclreclem3  14419  isercoll  15024  summolem2a  15072  fsumcvg3  15086  fsum2dlem  15125  fsumcom2  15129  qshash  15182  prodmolem2a  15288  fprod2dlem  15334  fprodcom2  15338  bitsfzo  15782  1arith  16261  vdwlem2  16316  vdwlem6  16320  vdwlem8  16322  ramtlecl  16334  prmgaplem3  16387  prmgaplem4  16388  monhom  17005  epihom  17012  funcsetcres2  17353  funcestrcsetclem8  17397  funcsetcestrclem8  17412  psdmrn  17817  gsumwspan  18011  frmdss2  18028  sursubmefmnd  18061  injsubmefmnd  18062  trivsubgsnd  18306  ssnmz  18318  trivnsgd  18324  conjnmz  18392  symgvalstruct  18525  gex1  18716  sylow2alem1  18742  lsmless1x  18769  lsmless2x  18770  lsmub1x  18771  lsmub2x  18772  lsmmod  18801  lsmdisj2  18808  efgrelexlemb  18876  efgcpbllemb  18881  cntzcmn  18960  gsum2d2  19094  dprdub  19147  dprdss  19151  dprddisj2  19161  pgpfac1lem3  19199  kerf1ghm  19498  isdrng2  19512  subrguss  19550  subrgmre  19559  primefld0cl  19585  primefld1cl  19586  lssssr  19725  lsssssubg  19730  lssmre  19738  lbspss  19854  lspdisj  19897  lbsextlem2  19931  lidl1el  19991  drngnidl  20002  lpiss  20023  unitrrg  20066  mhpsubg  20340  zsssubrg  20603  qsssubdrg  20604  cnsubrg  20605  mulgrhm2  20646  znrrg  20712  ocvocv  20815  ocv2ss  20817  ocvin  20818  lsmcss  20836  cssmre  20837  pjcss  20860  lindfrn  20965  dmatsgrp  21108  scmatsgrp  21128  scmatsgrp1  21131  m2cpmrngiso  21366  bastg  21574  tgss  21576  tgtop  21581  tgidm  21588  en2top  21593  neisspw  21715  topssnei  21732  neiptopuni  21738  lpss3  21752  clslp  21756  tgrest  21767  ssrest  21784  restntr  21790  ordtbas2  21799  ordtbas  21800  cnss1  21884  cnss2  21885  cnsscnp  21887  cnrest2r  21895  cmpsublem  22007  cmpsub  22008  tgcmp  22009  cmpcld  22010  hauscmplem  22014  cnconn  22030  llyss  22087  nllyss  22088  restnlly  22090  restlly  22091  locfincmp  22134  locfincf  22139  kgenss  22151  kgenidm  22155  llycmpkgen2  22158  1stckgen  22162  kgen2ss  22163  kgencn3  22166  ptbasfi  22189  ptpjopn  22220  txdis  22240  txkgen  22260  xkoptsub  22262  xkopjcn  22264  txconn  22297  qtoptop2  22307  qtopuni  22310  qtopkgen  22318  basqtop  22319  tgqtop  22320  qtopss  22323  qtoprest  22325  qtopomap  22326  qtopcmap  22327  kqsat  22339  kqcldsat  22341  hmphdis  22404  isfild  22466  ssfg  22480  fgss  22481  fgss2  22482  fgfil  22483  fgabs  22487  filconn  22491  fgtr  22498  uzrest  22505  ufilmax  22515  ufileu  22527  filufint  22528  rnelfm  22561  fmfnfmlem2  22563  fmfnfmlem4  22565  flimss2  22580  flimss1  22581  flimclsi  22586  flimcf  22590  flimsncls  22594  fclssscls  22626  fclsss1  22630  fclsss2  22631  fclscf  22633  uffclsflim  22639  alexsublem  22652  alexsubALTlem3  22657  ptcmplem2  22661  ptcmplem3  22662  cnextf  22674  efmndtmd  22709  symgtgp  22714  cldsubg  22719  tsmscl  22743  haustsms2  22745  tgptsmscls  22758  tsmsxp  22763  restutop  22846  ustuqtop4  22853  utop2nei  22859  utop3cls  22860  ucncn  22894  xblss2ps  23011  xblss2  23012  xrsblre  23419  xrsmopn  23420  recld2  23422  zdis  23424  icccmplem2  23431  cncfss  23507  cnheiborlem  23562  htpycn  23581  phtpyhtpy  23590  pi1blem  23647  cphsscph  23858  cfilfcls  23881  iscmet3lem2  23899  iscmet2  23901  caussi  23904  equivcfil  23906  lmcau  23920  metsscmetcld  23922  hlhil  24050  ivthicc  24065  ovoliunnul  24114  ovolicopnf  24131  uniioombllem3  24192  dyadmbllem  24206  volsup2  24212  vitalilem2  24216  itg1addlem4  24306  itg10a  24317  itg1ge0a  24318  mbfi1fseqlem4  24325  itg2gt0  24367  limciun  24500  perfdvf  24509  cpnord  24541  dvcj  24556  dvlip2  24601  dvivth  24616  dvne0  24617  dvcnvre  24625  ply1lpir  24782  plyco0  24792  plyexmo  24912  abelth  25039  efif1o  25141  logno1  25230  efopnlem2  25251  loglesqrt  25350  lgamcvg2  25643  ppisval  25692  ppinprm  25740  chtnprm  25742  fsumvma  25800  dchrfi  25842  chtppilimlem2  26061  chebbnd2  26064  vmadivsumb  26070  rplogsumlem2  26072  dchrisumlem2  26077  vmalogdivsum2  26125  vmalogdivsum  26126  2vmadivsumlem  26127  selbergb  26136  selberg2b  26139  selberg3lem1  26144  selberg3lem2  26145  selberg3  26146  selberg4lem1  26147  selberg4  26148  pntrlog2bndlem2  26165  pntrlog2bndlem4  26167  uhgredgss  26927  usgruspgrb  26977  uhgrissubgr  27068  uhgrspansubgrlem  27083  uhgrspan1  27096  cusgredg  27217  usgredgsscusgredg  27252  ococss  29079  shsub1  29110  shless  29145  shmodsi  29175  pjhth  29179  spansnss  29357  spanpr  29366  spansnm0i  29436  pjjsi  29486  sumdmdii  30201  sumdmdlem  30204  sumdmdlem2  30205  cdj3lem1  30220  abrexss  30282  fnpreimac  30427  rnmposs  30430  unifi3  30459  uzssico  30518  ssnnssfz  30521  pwrssmgc  30691  pmtrcnel  30765  cycpmrn  30817  cyc3evpm  30824  cycpmgcl  30827  ringlsmss2  30985  prmidlssidl  31001  dimkerim  31083  extdg1id  31113  crefss  31173  cmpcref  31174  tpr2rico  31212  esumrnmpt2  31384  esumpcvgval  31394  ldsysgenld  31476  sigapildsys  31478  ldgenpisys  31482  cldssbrsiga  31503  measdivcstALTV  31541  mbfmcnt  31583  oddpwdc  31669  eulerpartlemgs2  31695  reprpmtf1o  31954  bnj1033  32298  bnj1398  32363  sconnpi1  32543  cvmscld  32577  cvmliftlem15  32602  satfrnmapom  32674  dfon2lem6  33090  fprlem2  33195  fnessref  33762  fgmin  33775  tailfb  33782  dissneqlem  34702  icoreresf  34714  rdglimss  34739  finxpreclem6  34758  lindsenlbs  34997  poimirlem11  35013  poimirlem12  35014  sstotbnd3  35159  prdstotbnd  35177  cntotbnd  35179  ismtyhmeo  35188  1idl  35409  lshpdisj  36228  lssats  36253  lkrin  36405  glbconxN  36619  paddss1  37058  paddss2  37059  paddasslem16  37076  paddidm  37082  pmodlem2  37088  pmapjoin  37093  pmapjat1  37094  pclfinN  37141  pclfinclN  37191  diasslssN  38300  dia2dimlem12  38316  dihsslss  38517  baerlem3lem2  38951  baerlem5alem2  38952  baerlem5blem2  38953  eldiophss  39631  rencldnfilem  39677  pellexlem5  39690  pell14qrss1234  39713  pell1qrss14  39725  pellfundre  39738  pellfundge  39739  pellfundlb  39741  pellfundglb  39742  harinf  39891  proot1hash  40060  intabssd  40143  ss2iundf  40276  ov2ssiunov2  40317  clsk1indlem3  40665  finnzfsuppd  40835  radcnvrat  40938  nznngen  40940  trsspwALT3  41446  sspwimpALT2  41554  refsumcn  41579  iinssf  41698  icoiccdif  42087  icccncfext  42455  stoweidlem27  42595  stoweidlem46  42614  stoweidlem57  42625  fourierdlem40  42715  fourierdlem78  42752  ffnafv  43653  iccpartrn  43873  sprsymrelfvlem  43933  sprsymrelf1lem  43934  rnghmsscmap2  44523  rnghmsscmap  44524  funcrngcsetc  44548  funcrngcsetcALT  44549  rhmsscmap2  44569  rhmsscmap  44570  rhmsscrnghm  44576  rngcresringcat  44580  funcringcsetc  44585  funcringcsetcALTV2lem8  44593  funcringcsetclem8ALTV  44616  rhmsubcALTVlem4  44657  ssnn0ssfz  44677  lincolss  44769  lcoss  44771  lcosslsp  44773  iunord  45132
  Copyright terms: Public domain W3C validator