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

Theorem ssriv 3508
Description: Inference rule based on subclass definition. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
ssriv.1  |-  ( x  e.  A  ->  x  e.  B )
Assertion
Ref Expression
ssriv  |-  A  C_  B
Distinct variable groups:    x, A    x, B

Proof of Theorem ssriv
StepHypRef Expression
1 dfss2 3493 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 ssriv.1 . 2  |-  ( x  e.  A  ->  x  e.  B )
31, 2mpgbir 1605 1  |-  A  C_  B
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  ssid  3523  ssv  3524  difss  3631  ssun1  3667  inss1  3718  0ss  3814  difprsnss  4162  snsspw  4198  uniin  4265  iuniin  4336  iunpwss  4415  pwuni  4678  pwunss  4785  xpsspw  5116  dmin  5210  dmrnssfld  5261  dmcoss  5262  dminss  5420  imainss  5421  fviss  5925  mapsspm  7452  pmsspw  7453  uniixp  7492  pwfilem  7814  dffi3  7891  dfom3  8064  onwf  8248  tcrank  8302  cardprclem  8360  alephsson  8481  ackbij1  8618  cardcf  8632  cfeq0  8636  dfacfin7  8779  hsmexlem6  8811  canthnum  9027  inaprc  9214  nqerf  9308  addnqf  9326  mulnqf  9327  dmrecnq  9346  reclem2pr  9426  wuncn  9547  zssre  10871  zsscn  10872  nnssz  10884  elq  11184  zssq  11189  qssre  11192  rpssre  11230  ixxssixx  11543  iooval2  11562  ioossre  11586  rge0ssre  11628  fzssuz  11724  fzssp1  11726  uzdisj  11751  nn0disj  11788  fzossfz  11814  fzouzsplit  11828  fzossnn  11838  fzo0ssnn0  11864  uzrdgfni  12037  seqcoll  12478  wrdexg  12523  wrdexb  12524  fclim  13339  isercolllem3  13452  isercoll  13453  fsumge0  13572  climcnds  13626  divcnv  13628  harmonic  13633  mertenslem1  13656  bitsss  13935  maxprmfct  14113  prminf  14292  prmreclem2  14294  prmreclem3  14295  1arithlem1  14300  1arith  14304  4sqlem19  14340  vdwlem12  14369  restsspw  14687  xpsc0  14815  xpsc1  14816  mremre  14859  mreacs  14913  isfunc  15091  homarel  15221  ledm  15711  lern  15712  prdsgrpd  15989  prdsinvgd  15990  symgtrf  16300  odf1o2  16399  sylow3lem3  16455  sylow3lem6  16458  oppglsm  16468  efgsfo  16563  0frgp  16603  prdscmnd  16670  prdsabld  16671  gsummptnn0fz  16817  dprdssv  16858  dprdres  16877  ablfac1b  16923  prdsrngd  17062  prdscrngd  17063  unitss  17110  subrgint  17251  lssintcl  17410  prdslmodd  17415  psrbaglefi  17822  psrbaglefiOLD  17823  coe1mul2lem2  18108  xrge0subm  18255  cnsubmlem  18262  cnsubglem  18263  cnsubdrglem  18265  cnmsubglem  18276  zringlpir  18307  zlpir  18312  zringunit  18315  zrngunit  18316  znf1o  18385  zntoslem  18390  ocvss  18496  dsmmsubg  18569  dsmmlss  18570  lbslinds  18663  cldss2  19325  indiscld  19386  toponmre  19388  iscldtop  19390  1stcfb  19740  llyssnlly  19773  llyidm  19783  nllyidm  19784  toplly  19785  hauslly  19787  lly1stc  19791  1stckgenlem  19817  txindis  19898  pthaus  19902  ptcmpfi  20077  ufinffr  20193  cnflf2  20267  flimfcls  20290  alexsubALTlem3  20312  ptcmplem1  20315  ptcmpg  20320  prdstmdd  20385  prdstgpd  20386  ust0  20485  prdsms  20797  qdensere  21040  blssioo  21063  tgioo  21064  xrtgioo  21074  xrsmopn  21080  zdis  21084  reperflem  21086  xrge0gsumle  21101  xrge0tsms  21102  icopnfhmeo  21206  bndth  21221  ovoliunlem1  21676  ovoliun2  21680  ovolicc2lem4  21694  voliunlem2  21724  voliunlem3  21725  iunmbl  21726  uniioovol  21751  uniioombllem4  21758  vitali  21785  ismbf3d  21824  itg2seq  21912  itg2monolem1  21920  itg2monolem2  21921  itg2monolem3  21922  itg2mono  21923  itg2i1fseqle  21924  itg2i1fseq3  21927  itg2addlem  21928  itg2gt0  21930  itg2cnlem2  21932  limccl  22042  limcresi  22052  dvef  22144  plypf1  22372  aasscn  22476  qssaa  22482  aannenlem1  22486  aannenlem2  22487  aannenlem3  22488  ulmcn  22556  mtestbdd  22562  iblulm  22564  reeff1o  22604  reefgim  22607  efifo  22695  dfrelog  22709  relogf1o  22710  logdmss  22779  logcn  22784  dvloglem  22785  logf1o2  22787  dvlog  22788  dvlog2lem  22789  dvlog2  22790  logtayl  22797  cxpcn  22875  cxpcn2  22876  cxpcn3  22878  resqrtcn  22879  efrlim  23055  dfef2  23056  cxp2lim  23062  jensen  23074  wilthlem2  23099  wilthlem3  23100  basellem3  23112  basellem4  23113  prmdvdsfi  23137  vmaval  23143  mumul  23211  sqff1o  23212  musum  23223  fsumvma2  23245  dchrmhm  23272  chtppilim  23416  chto1lb  23419  chpchtlim  23420  chpo1ub  23421  dchrisumlema  23429  dchrmusum2  23435  dchrvmasum2lem  23437  dirith2  23469  mudivsum  23471  mulogsum  23473  mulog2sumlem2  23476  selberg2lem  23491  selberg3lem2  23499  pntrsumo1  23506  pnt2  23554  pnt  23555  axcontlem2  23972  axcontlem10  23980  usgraexmpl  24105  wwlksswrd  24392  wwlksswwlkn  24407  clwlksarewlks  24463  iseupa  24669  phrel  25434  bnrel  25487  hlrel  25510  shex  25833  chsssh  25847  hhssnv  25884  choc1  25949  shunssi  25990  shsleji  25992  shsub1i  25994  shsub2i  25995  shsidmi  26006  omlsii  26025  spanuni  26166  spansni  26179  5oalem7  26282  3oalem3  26286  pjrni  26324  mayete3i  26350  mayete3iOLD  26351  hmopex  26498  cnlnssadj  26703  adjbdln  26706  adjsslnop  26710  shatomistici  26984  hatomistici  26985  xrge0tsmsd  27466  esumpcvgval  27752  hashf2  27758  insiga  27805  sxbrsigalem0  27910  dya2icobrsiga  27915  sxbrsigalem1  27924  sxbrsigalem2  27925  eulerpartlemb  27975  lgamgulm2  28246  lgamcvglem  28250  erdszelem9  28311  erdsze2lem2  28316  kur14lem9  28326  ptpcon  28346  iinllycon  28367  cvmlift3  28441  imagesset  29208  altxpsspw  29232  bpolylem  29415  onsstopbas  29499  onsucconi  29507  onintopsscon  29510  onint1  29519  oninhaus  29520  itg2addnc  29674  itg2gt0cn  29675  ftc1anclem3  29697  ftc1anclem6  29700  ftc1anclem8  29702  topjoin  29814  heiborlem3  29940  eldioph3b  30330  diophin  30338  diophun  30339  eldiophss  30340  fz1ssnn  30376  isnumbasabl  30687  isnumbasgrp  30688  dfacbasgrp  30689  mon1psubm  30799  nzin  30851  rrpsscn  31166  icccncfext  31254  stoweidlem34  31362  stirlinglem13  31414  dirkeritg  31430  fourierdlem20  31455  fourierdlem39  31474  fourierdlem51  31486  fourierdlem57  31492  fourierdlem62  31497  fourierdlem64  31499  fourierdlem72  31507  fourierdlem73  31508  fourierdlem74  31509  fourierdlem77  31512  fourierdlem83  31518  fourierdlem89  31524  fourierdlem91  31526  fourierdlem93  31528  fourierdlem101  31536  fourierdlem103  31538  fourierdlem104  31539  fourierdlem111  31546  fouriersw  31560  lvecpsslmod  32207  unipwrVD  32730  unipwr  32731  bnj1398  33187  bnj1498  33214  bj-snglss  33627  bj-modssabl  33748  atssbase  34105
  Copyright terms: Public domain W3C validator