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

Theorem ssriv 3571
Description: Inference rule based on subclass definition. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
ssriv.1 (𝑥𝐴𝑥𝐵)
Assertion
Ref Expression
ssriv 𝐴𝐵
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem ssriv
StepHypRef Expression
1 dfss2 3556 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 ssriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1716 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  ssid  3586  ssv  3587  difss  3698  ssun1  3737  inss1  3794  0ss  3923  difprsnss  4269  snsspw  4310  uniin  4387  iuniin  4461  iunpwss  4545  pwuni  4819  pwunss  4932  dmin  5240  dmrnssfld  5291  dmcoss  5292  dminss  5451  imainss  5452  fviss  6150  mapsspm  7754  pmsspw  7755  uniixp  7794  pwfilem  8120  dffi3  8197  dfom3  8404  onwf  8553  tcrank  8607  cardprclem  8665  alephsson  8783  ackbij1  8920  cardcf  8934  cfeq0  8938  dfacfin7  9081  hsmexlem6  9113  canthnum  9327  inaprc  9514  nqerf  9608  addnqf  9626  mulnqf  9627  dmrecnq  9646  reclem2pr  9726  wuncn  9847  zssre  11219  zsscn  11220  nnssz  11232  elq  11624  zssq  11629  qssre  11632  rpssre  11677  ixxssixx  12018  iooval2  12037  ioossre  12064  rge0ssre  12109  fzssz  12171  fz1ssnn  12200  fzssuz  12210  fzssp1  12212  uzdisj  12239  fz0ssnn0  12261  nn0disj  12281  fzossfz  12314  fzouzsplit  12329  fzossnn  12341  fzo0ssnn0  12372  fzo0ssnn0OLD  12373  uzrdgfni  12576  seqcoll  13059  wrdexg  13118  wrdexb  13119  fclim  14080  isercolllem3  14193  isercoll  14194  climcnds  14370  divcnv  14372  harmonic  14378  fprodge0  14511  bitsss  14934  prmssnn  15176  maxprmfct  15207  prminf  15405  prmreclem3  15408  1arithlem1  15413  1arith  15417  4sqlem19  15453  vdwlem12  15482  restsspw  15863  xpsc0  15991  xpsc1  15992  mremre  16035  mreacs  16090  isfunc  16295  homarel  16457  ledm  16995  lern  16996  sgrpssmgm  17191  mndsssgrp  17192  prdsgrpd  17296  prdsinvgd  17297  symgtrf  17660  odf1o2  17759  sylow3lem3  17815  sylow3lem6  17818  oppglsm  17828  efgsfo  17923  0frgp  17963  prdscmnd  18035  prdsabld  18036  dprdssv  18186  dprdres  18198  ablfac1b  18240  prdsringd  18383  prdscrngd  18384  unitss  18431  subrgint  18573  lssintcl  18733  prdslmodd  18738  xrge0subm  19554  cnsubmlem  19561  cnsubglem  19562  cnsubdrglem  19564  cnmsubglem  19576  zringlpir  19602  zringunit  19605  znf1o  19666  zntoslem  19671  ocvss  19780  dsmmsubg  19853  dsmmlss  19854  lbslinds  19938  unitg  20529  cldss2  20591  indiscld  20652  toponmre  20654  iscldtop  20656  1stcfb  21005  llyssnlly  21038  llyidm  21048  nllyidm  21049  toplly  21050  hauslly  21052  lly1stc  21056  dissnref  21088  1stckgenlem  21113  txindis  21194  pthaus  21198  ptcmpfi  21373  ufinffr  21490  cnflf2  21564  flimfcls  21587  alexsubALTlem3  21610  ptcmplem1  21613  ptcmpg  21618  prdstmdd  21684  prdstgpd  21685  ust0  21780  prdsms  22093  qdensere  22330  blssioo  22353  tgioo  22354  xrtgioo  22364  xrsmopn  22370  zdis  22374  reperflem  22376  xrge0gsumle  22391  xrge0tsms  22392  icopnfhmeo  22497  bndth  22512  ovoliunlem1  23021  ovoliun2  23025  ovolicc2lem4  23039  voliunlem2  23070  voliunlem3  23071  uniioovol  23097  uniioombllem4  23104  vitali  23132  ismbf3d  23171  itg2seq  23259  limccl  23389  limcresi  23399  dvef  23491  aasscn  23821  qssaa  23827  aannenlem2  23832  aannenlem3  23833  ulmcn  23901  mtestbdd  23907  iblulm  23909  reeff1o  23949  reefgim  23952  efifo  24041  dfrelog  24060  relogf1o  24061  logdmss  24132  logcn  24137  dvloglem  24138  logf1o2  24140  dvlog  24141  dvlog2lem  24142  dvlog2  24143  logtayl  24150  cxpcn  24230  cxpcn2  24231  cxpcn3  24233  resqrtcn  24234  efrlim  24440  dfef2  24441  cxp2lim  24447  wilthlem2  24539  wilthlem3  24540  basellem3  24553  basellem4  24554  prmdvdsfi  24577  vmaval  24583  mumul  24651  sqff1o  24652  musum  24661  fsumvma2  24683  dchrmhm  24710  chtppilim  24908  chto1lb  24911  chpchtlim  24912  chpo1ub  24913  dchrisumlema  24921  dchrmusum2  24927  dchrvmasum2lem  24929  dirith2  24961  mudivsum  24963  mulogsum  24965  mulog2sumlem2  24968  selberg2lem  24983  selberg3lem2  24991  pntrsumo1  24998  pnt2  25046  pnt  25047  axcontlem2  25590  usgraexmplef  25722  wwlksswrd  26009  wwlksswwlkn  26024  clwlksarewlks  26080  phrel  26847  bnrel  26900  hlrel  26923  shex  27246  chsssh  27259  hhssnv  27298  choc1  27363  shunssi  27404  shsleji  27406  shsub1i  27408  shsub2i  27409  shsidmi  27420  omlsii  27439  spanuni  27580  spansni  27593  5oalem7  27696  3oalem3  27700  pjrni  27738  mayete3i  27764  hmopex  27911  cnlnssadj  28116  adjbdln  28119  adjsslnop  28123  shatomistici  28397  hatomistici  28398  xrge0tsmsd  28909  esumpcvgval  29260  hashf2  29266  insiga  29320  sigapisys  29338  sigaldsys  29342  sigapildsys  29345  sxbrsigalem0  29453  dya2icobrsiga  29458  sxbrsigalem1  29467  sxbrsigalem2  29468  eulerpartlemb  29550  bnj1398  30149  bnj1498  30176  erdszelem9  30228  erdsze2lem2  30233  kur14lem9  30243  ptpcon  30262  iinllycon  30283  cvmlift3  30357  mppsthm  30523  imagesset  31023  altxpsspw  31047  topjoin  31323  onsstopbas  31391  onsucconi  31399  onintopsscon  31402  onint1  31411  oninhaus  31412  bj-snglss  31934  bj-modssabl  32102  icoreunrn  32166  poimirlem8  32370  poimirlem18  32380  poimirlem21  32383  poimirlem22  32384  poimirlem31  32393  poimirlem32  32394  heiborlem3  32565  atssbase  33378  eldioph3b  36129  diophin  36137  diophun  36138  eldiophss  36139  isnumbasabl  36478  isnumbasgrp  36479  dfacbasgrp  36480  mon1psubm  36586  inintabss  36686  intimass  36748  nzin  37322  unipwrVD  37872  unipwr  37873  supxrre3  38265  fsumiunss  38425  rrpsscn  38438  dvnmul  38616  dvnprodlem2  38620  stoweidlem34  38710  stirlinglem13  38762  fourierdlem20  38803  fourierdlem62  38844  fourierdlem83  38865  fourierdlem101  38883  fourierdlem103  38885  fourierdlem104  38886  fourierdlem111  38893  fouriersw  38907  qndenserrnbllem  38973  sge0iunmptlemre  39091  nn0ssge0  39100  sge0isum  39103  sge0seq  39122  sge0reuz  39123  caragendifcl  39187  carageniuncllem2  39195  hoicvrrex  39229  smfaddlem1  39432  smfaddlem2  39433  mbfpsssmf  39452  griedg0ssusgr  40470  uvtxassvtx  40597  rgrusgrprc  40770  clwlks1wlks  40964  wwlkssswrd  41039  wwlkssswwlksn  41043  wspthsswwlkn  41106  wspthsswwlknon  41109  clwwlkssclwwlksn  41181  ringssrng  41651  srhmsubc  41849  srhmsubcALTV  41868  lvecpsslmod  42071  aacllem  42298  amgmwlem  42299  amgmlemALT  42300
  Copyright terms: Public domain W3C validator