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

Theorem ssriv 3754
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 3738 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 ssriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1873 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2144  wss 3721
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-in 3728  df-ss 3735
This theorem is referenced by:  ssid  3771  ssv  3772  difss  3886  ssun1  3925  inss1  3979  0ss  4114  difprsnss  4463  snsspw  4505  uniin  4592  pwuni  4608  iuniin  4663  iunpwss  4750  pwunss  5152  relopabi  5384  dmin  5470  dmrnssfld  5522  dmcoss  5523  dminss  5688  imainss  5689  fviss  6398  mapsspm  8042  pmsspw  8043  uniixp  8084  pwfilem  8415  dffi3  8492  dfom3  8707  onwf  8856  tcrank  8910  djuss  8945  djuunxp  8946  djuun  8951  cardprclem  9004  alephsson  9122  ackbij1  9261  cardcf  9275  cfeq0  9279  dfacfin7  9422  hsmexlem6  9454  canthnum  9672  inaprc  9859  nqerf  9953  addnqf  9971  mulnqf  9972  dmrecnq  9991  reclem2pr  10071  wuncn  10192  zssre  11585  zsscn  11586  nnssz  11598  elq  11992  zssq  11997  qssre  12000  rpssre  12045  ixxssixx  12393  iooval2  12412  ioossre  12439  rge0ssre  12486  fzssz  12549  fz1ssnn  12578  fzssuz  12588  fzssp1  12590  uzdisj  12619  fz0ssnn0  12641  nn0disj  12662  fzossfz  12695  fzouzsplit  12710  fzossnn  12724  fzo0ssnn0  12756  uzrdgfni  12964  seqcoll  13449  wrdexg  13510  wrdexb  13511  fclim  14491  isercolllem3  14604  isercoll  14605  climcnds  14789  divcnv  14791  harmonic  14797  fprodge0  14929  bitsss  15355  prmssnn  15596  maxprmfct  15627  prminf  15825  prmreclem3  15828  1arithlem1  15833  1arith  15837  4sqlem19  15873  vdwlem12  15902  restsspw  16299  xpsc0  16427  xpsc1  16428  mremre  16471  mreacs  16525  isfunc  16730  homarel  16892  ledm  17431  lern  17432  sgrpssmgm  17627  mndsssgrp  17628  prdsgrpd  17732  prdsinvgd  17733  symgtrf  18095  odf1o2  18194  sylow3lem3  18250  sylow3lem6  18253  oppglsm  18263  efgsfo  18358  0frgp  18398  prdscmnd  18470  prdsabld  18471  dprdssv  18622  dprdres  18634  ablfac1b  18676  prdsringd  18819  prdscrngd  18820  unitss  18867  subrgint  19011  lssintcl  19176  prdslmodd  19181  xrge0subm  20001  cnsubmlem  20008  cnsubglem  20009  cnsubdrglem  20011  cnmsubglem  20023  zringunit  20050  zringlpir  20051  znf1o  20114  zntoslem  20119  ocvss  20230  dsmmsubg  20303  dsmmlss  20304  lbslinds  20388  unitg  20991  cldss2  21054  indiscld  21115  toponmre  21117  iscldtop  21119  1stcfb  21468  llyssnlly  21501  llyidm  21511  nllyidm  21512  toplly  21513  hauslly  21515  lly1stc  21519  dissnref  21551  1stckgenlem  21576  txindis  21657  pthaus  21661  ptcmpfi  21836  ufinffr  21952  cnflf2  22026  flimfcls  22049  alexsubALTlem3  22072  ptcmplem1  22075  ptcmpg  22080  prdstmdd  22146  prdstgpd  22147  ust0  22242  prdsms  22555  qdensere  22792  blssioo  22817  tgioo  22818  xrtgioo  22828  xrsmopn  22834  zdis  22838  reperflem  22840  xrge0gsumle  22855  xrge0tsms  22856  icopnfhmeo  22961  bndth  22976  ovoliunlem1  23489  ovoliun2  23493  ovolicc2lem4  23507  voliunlem2  23538  voliunlem3  23539  uniioovol  23566  uniioombllem4  23573  vitali  23600  ismbf3d  23640  itg2seq  23728  limccl  23858  limcresi  23868  dvef  23962  aasscn  24292  qssaa  24298  aannenlem2  24303  aannenlem3  24304  ulmcn  24372  mtestbdd  24378  iblulm  24380  reeff1o  24420  reefgim  24423  efifo  24513  dfrelog  24532  relogf1o  24533  logdmss  24608  logcn  24613  dvloglem  24614  logf1o2  24616  dvlog  24617  dvlog2lem  24618  dvlog2  24619  logtayl  24626  cxpcn  24706  cxpcn2  24707  cxpcn3  24709  resqrtcn  24710  efrlim  24916  dfef2  24917  cxp2lim  24923  wilthlem2  25015  wilthlem3  25016  basellem3  25029  basellem4  25030  prmdvdsfi  25053  vmaval  25059  mumul  25127  sqff1o  25128  musum  25137  fsumvma2  25159  dchrmhm  25186  chtppilim  25384  chto1lb  25387  chpchtlim  25388  chpo1ub  25389  dchrisumlema  25397  dchrmusum2  25403  dchrvmasum2lem  25405  dirith2  25437  mudivsum  25439  mulogsum  25441  mulog2sumlem2  25444  selberg2lem  25459  selberg3lem2  25467  pntrsumo1  25474  pnt2  25522  pnt  25523  axcontlem2  26065  usgrexmplef  26373  griedg0ssusgr  26379  nbgrssvtx  26458  nbgrssovtx  26479  uvtxssvtx  26516  rgrusgrprc  26719  clwlkswks  26906  wwlkssswrd  26995  wwlkssswwlksn  26999  wspthsswwlkn  27062  wspthsswwlknon  27065  clwwlksclwwlkn  27183  phrel  28004  bnrel  28057  hlrel  28080  shex  28403  chsssh  28416  hhssnv  28455  choc1  28520  shunssi  28561  shsleji  28563  shsub1i  28565  shsub2i  28566  shsidmi  28577  omlsii  28596  spanuni  28737  spansni  28750  5oalem7  28853  3oalem3  28857  pjrni  28895  mayete3i  28921  hmopex  29068  cnlnssadj  29273  adjbdln  29276  adjsslnop  29280  shatomistici  29554  hatomistici  29555  xrge0tsmsd  30119  esumpcvgval  30474  hashf2  30480  insiga  30534  sigapisys  30552  sigaldsys  30556  sigapildsys  30559  sxbrsigalem0  30667  dya2icobrsiga  30672  sxbrsigalem1  30681  sxbrsigalem2  30682  eulerpartlemb  30764  chtvalz  31041  logdivsqrle  31062  bnj1398  31434  bnj1498  31461  erdszelem9  31513  erdsze2lem2  31518  kur14lem9  31528  ptpconn  31547  iinllyconn  31568  cvmlift3  31642  mppsthm  31808  imagesset  32391  altxpsspw  32415  topjoin  32691  onsstopbas  32759  onsucconni  32767  onintopssconn  32770  onint1  32779  oninhaus  32780  bj-snglss  33283  bj-modssabl  33472  icoreunrn  33537  poimirlem8  33743  poimirlem18  33753  poimirlem21  33756  poimirlem22  33757  poimirlem31  33766  poimirlem32  33767  heiborlem3  33937  atssbase  35092  eldioph3b  37847  diophin  37855  diophun  37856  eldiophss  37857  isnumbasabl  38195  isnumbasgrp  38196  dfacbasgrp  38197  mon1psubm  38303  inintabss  38403  intimass  38465  nzin  39036  unipwrVD  39583  unipwr  39584  supxrre3  40051  fsumiunss  40319  rrpsscn  40332  dvnmul  40670  dvnprodlem2  40674  stoweidlem34  40762  stirlinglem13  40814  fourierdlem20  40855  fourierdlem62  40896  fourierdlem83  40917  fourierdlem101  40935  fourierdlem103  40937  fourierdlem104  40938  fourierdlem111  40945  fouriersw  40959  qndenserrnbllem  41025  sge0iunmptlemre  41143  nn0ssge0  41152  sge0isum  41155  sge0seq  41174  sge0reuz  41175  caragendifcl  41242  carageniuncllem2  41250  hoicvrrex  41284  smfaddlem1  41485  smfaddlem2  41486  mbfpsssmf  41505  ringssrng  42398  srhmsubc  42594  srhmsubcALTV  42612  lvecpsslmod  42814  aacllem  43068  amgmwlem  43069  amgmlemALT  43070
  Copyright terms: Public domain W3C validator