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

Theorem ssriv 3640
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 3624 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 ssriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1766 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  ssid  3657  ssv  3658  difss  3770  ssun1  3809  inss1  3866  0ss  4005  difprsnss  4361  snsspw  4407  uniin  4489  pwuni  4506  iuniin  4563  iunpwss  4650  pwunss  5048  relopabi  5278  dmin  5364  dmrnssfld  5416  dmcoss  5417  dminss  5582  imainss  5583  fviss  6295  mapsspm  7933  pmsspw  7934  uniixp  7973  pwfilem  8301  dffi3  8378  dfom3  8582  onwf  8731  tcrank  8785  cardprclem  8843  alephsson  8961  ackbij1  9098  cardcf  9112  cfeq0  9116  dfacfin7  9259  hsmexlem6  9291  canthnum  9509  inaprc  9696  nqerf  9790  addnqf  9808  mulnqf  9809  dmrecnq  9828  reclem2pr  9908  wuncn  10029  zssre  11422  zsscn  11423  nnssz  11435  elq  11828  zssq  11833  qssre  11836  rpssre  11881  ixxssixx  12227  iooval2  12246  ioossre  12273  rge0ssre  12318  fzssz  12381  fz1ssnn  12410  fzssuz  12420  fzssp1  12422  uzdisj  12451  fz0ssnn0  12473  nn0disj  12494  fzossfz  12527  fzouzsplit  12542  fzossnn  12556  fzo0ssnn0  12588  fzo0ssnn0OLD  12589  uzrdgfni  12797  seqcoll  13286  wrdexg  13347  wrdexb  13348  fclim  14328  isercolllem3  14441  isercoll  14442  climcnds  14627  divcnv  14629  harmonic  14635  fprodge0  14768  bitsss  15195  prmssnn  15437  maxprmfct  15468  prminf  15666  prmreclem3  15669  1arithlem1  15674  1arith  15678  4sqlem19  15714  vdwlem12  15743  restsspw  16139  xpsc0  16267  xpsc1  16268  mremre  16311  mreacs  16366  isfunc  16571  homarel  16733  ledm  17271  lern  17272  sgrpssmgm  17467  mndsssgrp  17468  prdsgrpd  17572  prdsinvgd  17573  symgtrf  17935  odf1o2  18034  sylow3lem3  18090  sylow3lem6  18093  oppglsm  18103  efgsfo  18198  0frgp  18238  prdscmnd  18310  prdsabld  18311  dprdssv  18461  dprdres  18473  ablfac1b  18515  prdsringd  18658  prdscrngd  18659  unitss  18706  subrgint  18850  lssintcl  19012  prdslmodd  19017  xrge0subm  19835  cnsubmlem  19842  cnsubglem  19843  cnsubdrglem  19845  cnmsubglem  19857  zringunit  19884  zringlpir  19885  znf1o  19948  zntoslem  19953  ocvss  20062  dsmmsubg  20135  dsmmlss  20136  lbslinds  20220  unitg  20819  cldss2  20882  indiscld  20943  toponmre  20945  iscldtop  20947  1stcfb  21296  llyssnlly  21329  llyidm  21339  nllyidm  21340  toplly  21341  hauslly  21343  lly1stc  21347  dissnref  21379  1stckgenlem  21404  txindis  21485  pthaus  21489  ptcmpfi  21664  ufinffr  21780  cnflf2  21854  flimfcls  21877  alexsubALTlem3  21900  ptcmplem1  21903  ptcmpg  21908  prdstmdd  21974  prdstgpd  21975  ust0  22070  prdsms  22383  qdensere  22620  blssioo  22645  tgioo  22646  xrtgioo  22656  xrsmopn  22662  zdis  22666  reperflem  22668  xrge0gsumle  22683  xrge0tsms  22684  icopnfhmeo  22789  bndth  22804  ovoliunlem1  23316  ovoliun2  23320  ovolicc2lem4  23334  voliunlem2  23365  voliunlem3  23366  uniioovol  23393  uniioombllem4  23400  vitali  23427  ismbf3d  23466  itg2seq  23554  limccl  23684  limcresi  23694  dvef  23788  aasscn  24118  qssaa  24124  aannenlem2  24129  aannenlem3  24130  ulmcn  24198  mtestbdd  24204  iblulm  24206  reeff1o  24246  reefgim  24249  efifo  24338  dfrelog  24357  relogf1o  24358  logdmss  24433  logcn  24438  dvloglem  24439  logf1o2  24441  dvlog  24442  dvlog2lem  24443  dvlog2  24444  logtayl  24451  cxpcn  24531  cxpcn2  24532  cxpcn3  24534  resqrtcn  24535  efrlim  24741  dfef2  24742  cxp2lim  24748  wilthlem2  24840  wilthlem3  24841  basellem3  24854  basellem4  24855  prmdvdsfi  24878  vmaval  24884  mumul  24952  sqff1o  24953  musum  24962  fsumvma2  24984  dchrmhm  25011  chtppilim  25209  chto1lb  25212  chpchtlim  25213  chpo1ub  25214  dchrisumlema  25222  dchrmusum2  25228  dchrvmasum2lem  25230  dirith2  25262  mudivsum  25264  mulogsum  25266  mulog2sumlem2  25269  selberg2lem  25284  selberg3lem2  25292  pntrsumo1  25299  pnt2  25347  pnt  25348  axcontlem2  25890  usgrexmplef  26196  griedg0ssusgr  26202  nbgrssvtx  26281  nbgrssovtx  26302  uvtxssvtx  26338  rgrusgrprc  26541  clwlkswks  26728  wwlkssswrd  26816  wwlkssswwlksn  26820  wspthsswwlkn  26883  wspthsswwlknon  26886  clwwlksclwwlkn  26993  phrel  27798  bnrel  27851  hlrel  27874  shex  28197  chsssh  28210  hhssnv  28249  choc1  28314  shunssi  28355  shsleji  28357  shsub1i  28359  shsub2i  28360  shsidmi  28371  omlsii  28390  spanuni  28531  spansni  28544  5oalem7  28647  3oalem3  28651  pjrni  28689  mayete3i  28715  hmopex  28862  cnlnssadj  29067  adjbdln  29070  adjsslnop  29074  shatomistici  29348  hatomistici  29349  xrge0tsmsd  29913  esumpcvgval  30268  hashf2  30274  insiga  30328  sigapisys  30346  sigaldsys  30350  sigapildsys  30353  sxbrsigalem0  30461  dya2icobrsiga  30466  sxbrsigalem1  30475  sxbrsigalem2  30476  eulerpartlemb  30558  chtvalz  30835  logdivsqrle  30856  bnj1398  31228  bnj1498  31255  erdszelem9  31307  erdsze2lem2  31312  kur14lem9  31322  ptpconn  31341  iinllyconn  31362  cvmlift3  31436  mppsthm  31602  imagesset  32185  altxpsspw  32209  topjoin  32485  onsstopbas  32553  onsucconni  32561  onintopssconn  32564  onint1  32573  oninhaus  32574  bj-snglss  33083  bj-modssabl  33272  icoreunrn  33337  poimirlem8  33547  poimirlem18  33557  poimirlem21  33560  poimirlem22  33561  poimirlem31  33570  poimirlem32  33571  heiborlem3  33742  atssbase  34895  eldioph3b  37645  diophin  37653  diophun  37654  eldiophss  37655  isnumbasabl  37993  isnumbasgrp  37994  dfacbasgrp  37995  mon1psubm  38101  inintabss  38201  intimass  38263  nzin  38834  unipwrVD  39381  unipwr  39382  supxrre3  39854  fsumiunss  40125  rrpsscn  40138  dvnmul  40476  dvnprodlem2  40480  stoweidlem34  40569  stirlinglem13  40621  fourierdlem20  40662  fourierdlem62  40703  fourierdlem83  40724  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fouriersw  40766  qndenserrnbllem  40832  sge0iunmptlemre  40950  nn0ssge0  40959  sge0isum  40962  sge0seq  40981  sge0reuz  40982  caragendifcl  41049  carageniuncllem2  41057  hoicvrrex  41091  smfaddlem1  41292  smfaddlem2  41293  mbfpsssmf  41312  ringssrng  42205  srhmsubc  42401  srhmsubcALTV  42419  lvecpsslmod  42621  aacllem  42875  amgmwlem  42876  amgmlemALT  42877
  Copyright terms: Public domain W3C validator