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

Theorem ssrdv 3972
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 1919 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfss2 3954 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 235 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526  wcel 2105  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951
This theorem is referenced by:  eqelssd  3987  sscon  4114  ssdif  4115  unss1  4154  ssrin  4209  eq0rdv  4356  elpwdifsn  4715  uniss  4853  intss1  4884  intmin  4889  intssuni  4891  iinssiun  4924  iunss1  4925  iinss1  4926  ss2iun  4929  ssiun  4962  ssiun2  4963  iinss  4972  iinss2  4973  iunxdif3  5009  sspwb  5333  pwssun  5449  relop  5715  dmss  5765  dmcosseq  5838  ssrnres  6029  sossfld  6037  predpo  6160  preddowncl  6169  tron  6208  tz7.7  6211  dffv2  6750  chfnrn  6812  fvn0ssdmfun  6835  fveqdmss  6839  dff3  6859  ffnfv  6875  f1imass  7013  ssorduni  7488  onint  7498  limsssuc  7553  limuni3  7555  limomss  7573  fo1stres  7706  fo2ndres  7707  fo2ndf  7808  fnse  7818  ressuppssdif  7842  suppss  7851  reldmtpos  7891  onfununi  7969  smoiun  7989  smorndom  7996  tz7.48-1  8070  tz7.49  8072  oaass  8177  qsss  8348  uniinqs  8367  pmss12g  8423  mapss  8442  ixpssmap2g  8480  ixpssmapg  8481  fineqv  8722  pssnn  8725  ssfii  8872  dffi2  8876  oismo  8993  unxpwdom2  9041  inf3lemd  9079  inf3lem1  9080  inf3lem6  9085  cantnflem3  9143  cantnf  9145  cnfcom3lem  9155  onssr1  9249  rankunb  9268  tcrank  9302  harcard  9396  carduni  9399  infxpenlem  9428  infpwfien  9477  dfac12r  9561  ackbij2lem1  9630  ackbij1lem18  9648  isfin1-3  9797  fin1a2lem11  9821  fin1a2lem13  9823  zorn2lem4  9910  zorn2lem5  9911  ttukeylem6  9925  ttukeylem7  9926  fpwwe2lem11  10051  fpwwe2lem12  10052  fpwwe2  10054  wunr1om  10130  wunom  10131  tskr1om  10178  tskr1om2  10179  tskxpss  10183  tskcard  10192  tskuni  10194  grothomex  10240  genpss  10415  distrlem1pr  10436  distrlem5pr  10438  ltexprlem2  10448  ltexprlem6  10452  ltexprlem7  10453  reclem3pr  10460  reclem4pr  10461  supaddc  11597  supadd  11598  supmul1  11599  supmullem2  11601  peano5uzi  12060  uzss  12254  ixxdisj  12743  ixxss1  12746  ixxss2  12747  ixxss12  12748  ixxub  12749  ixxlb  12750  iocssre  12806  icossre  12807  iccssre  12808  icodisj  12852  fzss1  12936  fzss2  12937  ssfzunsnext  12942  fzosplit  13060  fzouzsplit  13062  ssfzo12bi  13122  ssnn0fi  13343  fsuppmapnn0fiub  13349  suppssfz  13352  sswrd  13859  rtrclreclem3  14409  isercoll  15014  summolem2a  15062  fsumcvg3  15076  fsum2dlem  15115  fsumcom2  15119  qshash  15172  prodmolem2a  15278  fprod2dlem  15324  fprodcom2  15328  bitsfzo  15774  1arith  16253  vdwlem2  16308  vdwlem6  16312  vdwlem8  16314  ramtlecl  16326  prmgaplem3  16379  prmgaplem4  16380  monhom  16995  epihom  17002  funcsetcres2  17343  funcestrcsetclem8  17387  funcsetcestrclem8  17402  psdmrn  17807  gsumwspan  18001  frmdss2  18018  trivsubgsnd  18246  ssnmz  18258  trivnsgd  18264  conjnmz  18332  gex1  18647  sylow2alem1  18673  lsmless1x  18700  lsmless2x  18701  lsmub1x  18702  lsmub2x  18703  lsmmod  18732  lsmdisj2  18739  efgrelexlemb  18807  efgcpbllemb  18812  cntzcmn  18891  gsum2d2  19025  dprdub  19078  dprdss  19082  dprddisj2  19092  pgpfac1lem3  19130  kerf1ghm  19428  kerf1hrmOLD  19429  isdrng2  19443  subrguss  19481  subrgmre  19490  primefld0cl  19516  primefld1cl  19517  lssssr  19656  lsssssubg  19661  lssmre  19669  lbspss  19785  lspdisj  19828  lbsextlem2  19862  lidl1el  19921  drngnidl  19932  lpiss  19953  unitrrg  19996  mhpsubg  20270  zsssubrg  20533  qsssubdrg  20534  cnsubrg  20535  mulgrhm2  20576  znrrg  20642  ocvocv  20745  ocv2ss  20747  ocvin  20748  lsmcss  20766  cssmre  20767  pjcss  20790  lindfrn  20895  dmatsgrp  21038  scmatsgrp  21058  scmatsgrp1  21061  m2cpmrngiso  21296  bastg  21504  tgss  21506  tgtop  21511  tgidm  21518  en2top  21523  neisspw  21645  topssnei  21662  neiptopuni  21668  lpss3  21682  clslp  21686  tgrest  21697  ssrest  21714  restntr  21720  ordtbas2  21729  ordtbas  21730  cnss1  21814  cnss2  21815  cnsscnp  21817  cnrest2r  21825  cmpsublem  21937  cmpsub  21938  tgcmp  21939  cmpcld  21940  hauscmplem  21944  cnconn  21960  llyss  22017  nllyss  22018  restnlly  22020  restlly  22021  locfincmp  22064  locfincf  22069  kgenss  22081  kgenidm  22085  llycmpkgen2  22088  1stckgen  22092  kgen2ss  22093  kgencn3  22096  ptbasfi  22119  ptpjopn  22150  txdis  22170  txkgen  22190  xkoptsub  22192  xkopjcn  22194  txconn  22227  qtoptop2  22237  qtopuni  22240  qtopkgen  22248  basqtop  22249  tgqtop  22250  qtopss  22253  qtoprest  22255  qtopomap  22256  qtopcmap  22257  kqsat  22269  kqcldsat  22271  hmphdis  22334  isfild  22396  ssfg  22410  fgss  22411  fgss2  22412  fgfil  22413  fgabs  22417  filconn  22421  fgtr  22428  uzrest  22435  ufilmax  22445  ufileu  22457  filufint  22458  rnelfm  22491  fmfnfmlem2  22493  fmfnfmlem4  22495  flimss2  22510  flimss1  22511  flimclsi  22516  flimcf  22520  flimsncls  22524  fclssscls  22556  fclsss1  22560  fclsss2  22561  fclscf  22563  uffclsflim  22569  alexsublem  22582  alexsubALTlem3  22587  ptcmplem2  22591  ptcmplem3  22592  cnextf  22604  symgtgp  22639  cldsubg  22648  tsmscl  22672  haustsms2  22674  tgptsmscls  22687  tsmsxp  22692  restutop  22775  ustuqtop4  22782  utop2nei  22788  utop3cls  22789  ucncn  22823  xblss2ps  22940  xblss2  22941  xrsblre  23348  xrsmopn  23349  recld2  23351  zdis  23353  icccmplem2  23360  cncfss  23436  cnheiborlem  23487  htpycn  23506  phtpyhtpy  23515  pi1blem  23572  cphsscph  23783  cfilfcls  23806  iscmet3lem2  23824  iscmet2  23826  caussi  23829  equivcfil  23831  lmcau  23845  metsscmetcld  23847  hlhil  23975  ivthicc  23988  ovoliunnul  24037  ovolicopnf  24054  uniioombllem3  24115  dyadmbllem  24129  volsup2  24135  vitalilem2  24139  itg1addlem4  24229  itg10a  24240  itg1ge0a  24241  mbfi1fseqlem4  24248  itg2gt0  24290  limciun  24421  perfdvf  24430  cpnord  24461  dvcj  24476  dvlip2  24521  dvivth  24536  dvne0  24537  dvcnvre  24545  ply1lpir  24701  plyco0  24711  plyexmo  24831  abelth  24958  efif1o  25057  logno1  25146  efopnlem2  25167  loglesqrt  25266  lgamcvg2  25560  ppisval  25609  ppinprm  25657  chtnprm  25659  fsumvma  25717  dchrfi  25759  chtppilimlem2  25978  chebbnd2  25981  vmadivsumb  25987  rplogsumlem2  25989  dchrisumlem2  25994  vmalogdivsum2  26042  vmalogdivsum  26043  2vmadivsumlem  26044  selbergb  26053  selberg2b  26056  selberg3lem1  26061  selberg3lem2  26062  selberg3  26063  selberg4lem1  26064  selberg4  26065  pntrlog2bndlem2  26082  pntrlog2bndlem4  26084  uhgredgss  26844  usgruspgrb  26894  uhgrissubgr  26985  uhgrspansubgrlem  27000  uhgrspan1  27013  cusgredg  27134  usgredgsscusgredg  27169  ococss  28998  shsub1  29029  shless  29064  shmodsi  29094  pjhth  29098  spansnss  29276  spanpr  29285  spansnm0i  29355  pjjsi  29405  sumdmdii  30120  sumdmdlem  30123  sumdmdlem2  30124  cdj3lem1  30139  abrexss  30200  fnpreimac  30345  rnmposs  30348  unifi3  30375  uzssico  30434  ssnnssfz  30437  pmtrcnel  30661  cycpmrn  30713  cyc3evpm  30720  cycpmgcl  30723  dimkerim  30923  extdg1id  30953  crefss  31013  cmpcref  31014  tpr2rico  31055  esumrnmpt2  31227  esumpcvgval  31237  ldsysgenld  31319  sigapildsys  31321  ldgenpisys  31325  cldssbrsiga  31346  measdivcstALTV  31384  mbfmcnt  31426  oddpwdc  31512  eulerpartlemgs2  31538  reprpmtf1o  31797  bnj1033  32139  bnj1398  32204  sconnpi1  32384  cvmscld  32418  cvmliftlem15  32443  satfrnmapom  32515  dfon2lem6  32931  fprlem2  33036  fnessref  33603  fgmin  33616  tailfb  33623  dissneqlem  34504  icoreresf  34516  rdglimss  34541  finxpreclem6  34560  lindsenlbs  34769  poimirlem11  34785  poimirlem12  34786  sstotbnd3  34937  prdstotbnd  34955  cntotbnd  34957  ismtyhmeo  34966  1idl  35187  lshpdisj  36005  lssats  36030  lkrin  36182  glbconxN  36396  paddss1  36835  paddss2  36836  paddasslem16  36853  paddidm  36859  pmodlem2  36865  pmapjoin  36870  pmapjat1  36871  pclfinN  36918  pclfinclN  36968  diasslssN  38077  dia2dimlem12  38093  dihsslss  38294  baerlem3lem2  38728  baerlem5alem2  38729  baerlem5blem2  38730  qsalrel  39005  eldiophss  39251  rencldnfilem  39297  pellexlem5  39310  pell14qrss1234  39333  pell1qrss14  39345  pellfundre  39358  pellfundge  39359  pellfundlb  39361  pellfundglb  39362  harinf  39511  proot1hash  39680  intabssd  39765  ss2iundf  39884  ov2ssiunov2  39925  clsk1indlem3  40273  radcnvrat  40526  nznngen  40528  trsspwALT3  41034  sspwimpALT2  41142  refsumcn  41167  iinssf  41287  icoiccdif  41680  icccncfext  42050  stoweidlem27  42193  stoweidlem46  42212  stoweidlem57  42223  fourierdlem40  42313  fourierdlem78  42350  ffnafv  43251  iccpartrn  43437  sprsymrelfvlem  43499  sprsymrelf1lem  43500  sursubmefmnd  43963  injsubmefmnd  43964  efmndtmd  43967  rnghmsscmap2  44142  rnghmsscmap  44143  funcrngcsetc  44167  funcrngcsetcALT  44168  rhmsscmap2  44188  rhmsscmap  44189  rhmsscrnghm  44195  rngcresringcat  44199  funcringcsetc  44204  funcringcsetcALTV2lem8  44212  funcringcsetclem8ALTV  44235  rhmsubcALTVlem4  44276  ssnn0ssfz  44295  lincolss  44387  lcoss  44389  lcosslsp  44391  iunord  44677
  Copyright terms: Public domain W3C validator