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

Theorem ssrdv 3804
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 2018 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfss2 3786 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 225 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1635  wcel 2156  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783
This theorem is referenced by:  eqelssd  3819  sscon  3943  ssdif  3944  unss1  3981  ssrin  4034  eq0rdv  4177  elpwdifsn  4511  uniss  4653  intss1  4684  intmin  4689  intssuni  4691  iunss1  4724  iinss1  4725  ss2iun  4728  ssiun  4754  ssiun2  4755  iinss  4763  iinss2  4764  iunxdif3  4798  trintssOLD  4963  sspwb  5107  pwssun  5215  relop  5474  dmss  5524  dmcosseq  5588  ssrnres  5783  sossfld  5791  predpo  5911  preddowncl  5920  tron  5959  tz7.7  5962  dffv2  6492  chfnrn  6550  fvn0ssdmfun  6572  fveqdmss  6576  dff3  6594  ffnfv  6610  f1imass  6745  ssorduni  7215  onint  7225  limsssuc  7280  limuni3  7282  limomss  7300  fo1stres  7424  fo2ndres  7425  fo2ndf  7518  fnse  7528  ressuppssdif  7550  suppss  7560  reldmtpos  7595  onfununi  7674  smoiun  7694  smorndom  7701  tz7.48-1  7774  tz7.49  7776  oaass  7878  qsss  8043  uniinqs  8062  pmss12g  8119  mapss  8137  ixpssmap2g  8174  ixpssmapg  8175  fineqv  8414  pssnn  8417  ssfii  8564  dffi2  8568  oismo  8684  unxpwdom2  8732  inf3lemd  8771  inf3lem1  8772  inf3lem6  8777  cantnflem3  8835  cantnf  8837  cnfcom3lem  8847  onssr1  8941  rankunb  8960  tcrank  8994  harcard  9087  carduni  9090  infxpenlem  9119  infpwfien  9168  dfac12r  9253  ackbij2lem1  9326  ackbij1lem18  9344  isfin1-3  9493  fin1a2lem11  9517  fin1a2lem13  9519  zorn2lem4  9606  zorn2lem5  9607  ttukeylem6  9621  ttukeylem7  9622  fpwwe2lem11  9747  fpwwe2lem12  9748  fpwwe2  9750  wunr1om  9826  wunom  9827  tskr1om  9874  tskr1om2  9875  tskxpss  9879  tskcard  9888  tskuni  9890  grothomex  9936  genpss  10111  distrlem1pr  10132  distrlem5pr  10134  ltexprlem2  10144  ltexprlem6  10148  ltexprlem7  10149  reclem3pr  10156  reclem4pr  10157  supaddc  11275  supadd  11276  supmul1  11277  supmullem2  11279  peano5uzi  11732  uzss  11925  ixxdisj  12408  ixxss1  12411  ixxss2  12412  ixxss12  12413  ixxub  12414  ixxlb  12415  iocssre  12471  icossre  12472  iccssre  12473  icodisj  12518  fzss1  12603  fzss2  12604  ssfzunsnext  12609  fzosplit  12725  fzouzsplit  12727  ssfzo12bi  12787  ssnn0fi  13008  fsuppmapnn0fiub  13014  suppssfz  13017  sswrd  13524  rtrclreclem3  14023  isercoll  14621  summolem2a  14669  fsumcvg3  14683  fsum2dlem  14724  fsumcom2  14728  qshash  14781  prodmolem2a  14885  fprod2dlem  14931  fprodcom2  14935  bitsfzo  15376  1arith  15848  vdwlem2  15903  vdwlem6  15907  vdwlem8  15909  ramtlecl  15921  prmgaplem3  15974  prmgaplem4  15975  monhom  16599  epihom  16606  funcsetcres2  16947  funcestrcsetclem8  16992  funcsetcestrclem8  17007  psdmrn  17412  gsumwspan  17588  frmdss2  17605  ssnmz  17838  conjnmz  17896  gex1  18207  sylow2alem1  18233  lsmless1x  18260  lsmless2x  18261  lsmub1x  18262  lsmub2x  18263  lsmmod  18289  lsmdisj2  18296  efgrelexlemb  18364  efgcpbllemb  18369  cntzcmn  18446  gsum2d2  18574  dprdub  18626  dprdss  18630  dprddisj2  18640  pgpfac1lem3  18678  kerf1hrm  18947  isdrng2  18961  subrguss  18999  subrgmre  19008  lssssr  19159  lssssrOLD  19160  lsssssubg  19165  lssmre  19173  lbspss  19289  lspdisj  19332  lbsextlem2  19368  lidl1el  19427  drngnidl  19438  lpiss  19459  unitrrg  19502  zsssubrg  20012  qsssubdrg  20013  cnsubrg  20014  mulgrhm2  20055  znrrg  20121  ocvocv  20225  ocv2ss  20227  ocvin  20228  lsmcss  20246  cssmre  20247  pjcss  20270  lindfrn  20370  dmatsgrp  20516  scmatsgrp  20536  scmatsgrp1  20539  m2cpmrngiso  20776  bastg  20984  tgss  20986  tgtop  20991  tgidm  20998  en2top  21003  neisspw  21125  topssnei  21142  neiptopuni  21148  lpss3  21162  clslp  21166  tgrest  21177  ssrest  21194  restntr  21200  ordtbas2  21209  ordtbas  21210  cnss1  21294  cnss2  21295  cnsscnp  21297  cnrest2r  21305  cmpsublem  21416  cmpsub  21417  tgcmp  21418  cmpcld  21419  hauscmplem  21423  cnconn  21439  llyss  21496  nllyss  21497  restnlly  21499  restlly  21500  locfincmp  21543  locfincf  21548  kgenss  21560  kgenidm  21564  llycmpkgen2  21567  1stckgen  21571  kgen2ss  21572  kgencn3  21575  ptbasfi  21598  ptpjopn  21629  txdis  21649  txkgen  21669  xkoptsub  21671  xkopjcn  21673  txconn  21706  qtoptop2  21716  qtopuni  21719  qtopkgen  21727  basqtop  21728  tgqtop  21729  qtopss  21732  qtoprest  21734  qtopomap  21735  qtopcmap  21736  kqsat  21748  kqcldsat  21750  hmphdis  21813  isfild  21875  ssfg  21889  fgss  21890  fgss2  21891  fgfil  21892  fgabs  21896  filconn  21900  fgtr  21907  uzrest  21914  ufilmax  21924  ufileu  21936  filufint  21937  rnelfm  21970  fmfnfmlem2  21972  fmfnfmlem4  21974  flimss2  21989  flimss1  21990  flimclsi  21995  flimcf  21999  flimsncls  22003  fclssscls  22035  fclsss1  22039  fclsss2  22040  fclscf  22042  uffclsflim  22048  alexsublem  22061  alexsubALTlem3  22066  ptcmplem2  22070  ptcmplem3  22071  cnextf  22083  symgtgp  22118  cldsubg  22127  tsmscl  22151  haustsms2  22153  tgptsmscls  22166  tsmsxp  22171  restutop  22254  ustuqtop4  22261  utop2nei  22267  utop3cls  22268  ucncn  22302  xblss2ps  22419  xblss2  22420  xrsblre  22827  xrsmopn  22828  recld2  22830  zdis  22832  icccmplem2  22839  cncfss  22915  cnheiborlem  22966  htpycn  22985  phtpyhtpy  22994  pi1blem  23051  cfilfcls  23284  iscmet3lem2  23302  iscmet2  23304  caussi  23307  equivcfil  23309  lmcau  23323  cmetss  23325  hlhil  23426  ivthicc  23439  ovoliunnul  23488  ovolicopnf  23505  uniioombllem3  23566  dyadmbllem  23580  volsup2  23586  vitalilem2  23590  itg1addlem4  23680  itg10a  23691  itg1ge0a  23692  mbfi1fseqlem4  23699  itg2gt0  23741  limciun  23872  perfdvf  23881  cpnord  23912  dvcj  23927  dvlip2  23972  dvivth  23987  dvne0  23988  dvcnvre  23996  ply1lpir  24152  plyco0  24162  plyexmo  24282  abelth  24409  efif1o  24507  logno1  24596  efopnlem2  24617  loglesqrt  24713  lgamcvg2  24995  ppisval  25044  ppinprm  25092  chtnprm  25094  fsumvma  25152  dchrfi  25194  chtppilimlem2  25377  chebbnd2  25380  vmadivsumb  25386  rplogsumlem2  25388  dchrisumlem2  25393  vmalogdivsum2  25441  vmalogdivsum  25442  2vmadivsumlem  25443  selbergb  25452  selberg2b  25455  selberg3lem1  25460  selberg3lem2  25461  selberg3  25462  selberg4lem1  25463  selberg4  25464  pntrlog2bndlem2  25481  pntrlog2bndlem4  25483  uhgredgss  26240  usgruspgrb  26291  uhgrissubgr  26383  uhgrspansubgrlem  26398  uhgrspan1  26411  nbgrssvtxOLD  26454  nbgrssovtxOLD  26476  cusgredg  26548  usgredgsscusgredg  26583  ococss  28480  shsub1  28511  shless  28546  shmodsi  28576  pjhth  28580  spansnss  28758  spanpr  28767  spansnm0i  28837  pjjsi  28887  sumdmdii  29602  sumdmdlem  29605  sumdmdlem2  29606  cdj3lem1  29621  abrexss  29675  iinssiun  29702  rnmpt2ss  29800  unifi3  29817  uzssico  29873  ssnnssfz  29876  crefss  30241  cmpcref  30242  tpr2rico  30283  esumrnmpt2  30455  esumpcvgval  30465  ldsysgenld  30548  sigapildsys  30550  ldgenpisys  30554  cldssbrsiga  30575  measdivcstOLD  30612  mbfmcnt  30655  oddpwdc  30741  eulerpartlemgs2  30767  reprpmtf1o  31029  bnj1033  31360  bnj1398  31425  sconnpi1  31544  cvmscld  31578  cvmliftlem15  31603  dfon2lem6  32013  fnessref  32673  fgmin  32686  tailfb  32693  dissneqlem  33504  icoreresf  33516  finxpreclem6  33549  lindsenlbs  33717  poimirlem11  33733  poimirlem12  33734  sstotbnd3  33886  prdstotbnd  33904  cntotbnd  33906  ismtyhmeo  33915  1idl  34136  lshpdisj  34767  lssats  34792  lkrin  34944  glbconxN  35158  paddss1  35597  paddss2  35598  paddasslem16  35615  paddidm  35621  pmodlem2  35627  pmapjoin  35632  pmapjat1  35633  pclfinN  35680  pclfinclN  35730  diasslssN  36840  dia2dimlem12  36856  dihsslss  37057  baerlem3lem2  37491  baerlem5alem2  37492  baerlem5blem2  37493  eldiophss  37840  rencldnfilem  37886  pellexlem5  37899  pell14qrss1234  37922  pell1qrss14  37934  pellfundre  37947  pellfundge  37948  pellfundlb  37950  pellfundglb  37951  harinf  38102  proot1hash  38279  intabssd  38416  ss2iundf  38451  ov2ssiunov2  38492  clsk1indlem3  38841  radcnvrat  39013  nznngen  39015  trsspwALT3  39544  sspwimpALT2  39658  refsumcn  39683  iinssf  39818  icoiccdif  40231  icccncfext  40580  stoweidlem27  40723  stoweidlem46  40742  stoweidlem57  40753  fourierdlem40  40843  fourierdlem78  40880  ffnafv  41760  iccpartrn  41941  sprsymrelfvlem  42308  sprsymrelf1lem  42309  rnghmsscmap2  42541  rnghmsscmap  42542  funcrngcsetc  42566  funcrngcsetcALT  42567  rhmsscmap2  42587  rhmsscmap  42588  rhmsscrnghm  42594  rngcresringcat  42598  funcringcsetc  42603  funcringcsetcALTV2lem8  42611  funcringcsetclem8ALTV  42634  rhmsubcALTVlem4  42675  ssnn0ssfz  42695  lincolss  42791  lcoss  42793  lcosslsp  42795  iunord  42990
  Copyright terms: Public domain W3C validator