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

Theorem ssriv 3352
Description: Inference rule based on subclass definition. (Contributed by NM, 5-Aug-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 3337 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 ssriv.1 . 2  |-  ( x  e.  A  ->  x  e.  B )
31, 2mpgbir 1559 1  |-  A  C_  B
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725    C_ wss 3320
This theorem is referenced by:  ssid  3367  ssv  3368  difss  3474  ssun1  3510  inss1  3561  0ss  3656  difprsnss  3934  snsspw  3970  uniin  4035  iuniin  4103  iunpwss  4180  pwuni  4395  pwunss  4488  xpsspw  4986  dmin  5077  dmrnssfld  5129  dmcoss  5135  dminss  5286  imainss  5287  fviss  5784  mapsspm  7047  pmsspw  7048  uniixp  7085  pwfilem  7401  dffi3  7436  dfom3  7602  onwf  7756  tcrank  7808  cardprclem  7866  alephsson  7981  ackbij1  8118  cardcf  8132  cfeq0  8136  dfacfin7  8279  hsmexlem6  8311  canthnum  8524  inaprc  8711  nqerf  8807  addnqf  8825  mulnqf  8826  dmrecnq  8845  reclem2pr  8925  wuncn  9045  zssre  10289  zsscn  10290  nnssz  10301  elq  10576  zssq  10581  qssre  10584  rpssre  10622  ixxssixx  10930  iooval2  10949  ioossre  10972  fzssuz  11093  fzssp1  11095  uzdisj  11119  fzossfz  11157  fzouzsplit  11168  fzossnn  11172  uzrdgfni  11298  seqcoll  11712  wrdexg  11739  wrdexb  11763  fclim  12347  isercolllem3  12460  isercoll  12461  fsumge0  12574  climcnds  12631  divcnv  12633  harmonic  12638  mertenslem1  12661  bitsss  12938  maxprmfct  13113  prminf  13283  prmreclem2  13285  prmreclem3  13286  1arithlem1  13291  1arith  13295  4sqlem19  13331  vdwlem12  13360  restsspw  13659  xpsc0  13785  xpsc1  13786  mremre  13829  mreacs  13883  isfunc  14061  homarel  14191  ledm  14669  lern  14670  prdsgrpd  14927  prdsinvgd  14928  odf1o2  15207  sylow3lem3  15263  sylow3lem6  15266  oppglsm  15276  efgsfo  15371  0frgp  15411  prdscmnd  15476  prdsabld  15477  dprdssv  15574  dprdres  15586  ablfac1b  15628  prdsrngd  15718  prdscrngd  15719  unitss  15765  subrgint  15890  lssintcl  16040  prdslmodd  16045  psrbaglefi  16437  coe1mul2lem2  16661  xrge0subm  16739  cnsubmlem  16746  cnsubglem  16747  cnsubdrglem  16749  cnmsubglem  16761  zrngunit  16765  zlpir  16771  znf1o  16832  zntoslem  16837  ocvss  16897  cldss2  17094  indiscld  17155  toponmre  17157  iscldtop  17159  1stcfb  17508  llyssnlly  17541  llyidm  17551  nllyidm  17552  toplly  17553  hauslly  17555  lly1stc  17559  1stckgenlem  17585  txindis  17666  pthaus  17670  ptcmpfi  17845  ufinffr  17961  cnflf2  18035  flimfcls  18058  alexsubALTlem3  18080  ptcmplem1  18083  ptcmpg  18088  prdstmdd  18153  prdstgpd  18154  ust0  18249  prdsms  18561  qdensere  18804  blssioo  18826  tgioo  18827  xrtgioo  18837  xrsmopn  18843  zdis  18847  reperflem  18849  xrge0gsumle  18864  xrge0tsms  18865  icopnfhmeo  18968  bndth  18983  ovoliunlem1  19398  ovoliun2  19402  ovolicc2lem4  19416  voliunlem2  19445  voliunlem3  19446  iunmbl  19447  uniioovol  19471  uniioombllem4  19478  vitali  19505  ismbf3d  19546  itg2seq  19634  itg2monolem1  19642  itg2monolem2  19643  itg2monolem3  19644  itg2mono  19645  itg2i1fseqle  19646  itg2i1fseq3  19649  itg2addlem  19650  itg2gt0  19652  itg2cnlem2  19654  limccl  19762  limcresi  19772  dvef  19864  plypf1  20131  aasscn  20235  qssaa  20241  aannenlem1  20245  aannenlem2  20246  aannenlem3  20247  ulmcn  20315  mtestbdd  20321  iblulm  20323  reeff1o  20363  reefgim  20366  efifo  20449  dfrelog  20463  relogf1o  20464  logdmss  20533  logcn  20538  dvloglem  20539  logf1o2  20541  dvlog  20542  dvlog2lem  20543  dvlog2  20544  logtayl  20551  cxpcn  20629  cxpcn2  20630  cxpcn3  20632  resqrcn  20633  efrlim  20808  dfef2  20809  cxp2lim  20815  jensen  20827  wilthlem2  20852  wilthlem3  20853  basellem3  20865  basellem4  20866  prmdvdsfi  20890  vmaval  20896  vmaf  20902  mumul  20964  sqff1o  20965  musum  20976  fsumvma2  20998  dchrmhm  21025  chtppilim  21169  chto1lb  21172  chpchtlim  21173  chpo1ub  21174  dchrisumlema  21182  dchrmusum2  21188  dchrvmasum2lem  21190  dirith2  21222  mudivsum  21224  mulogsum  21226  mulog2sumlem2  21229  selberg2lem  21244  selberg3lem2  21252  pntrsumo1  21259  pnt2  21307  pnt  21308  usgraexmpl  21420  iseupa  21687  phrel  22316  bnrel  22369  hlrel  22392  shex  22714  chsssh  22728  hhssnv  22764  choc1  22829  shunssi  22870  shsleji  22872  shsub1i  22874  shsub2i  22875  shsidmi  22886  omlsii  22905  spanuni  23046  spansni  23059  5oalem7  23162  3oalem3  23166  pjrni  23204  mayete3i  23230  mayete3iOLD  23231  hmopex  23378  cnlnssadj  23583  adjbdln  23586  adjsslnop  23590  shatomistici  23864  hatomistici  23865  xrge0tsmsd  24223  esumpcvgval  24468  hashf2  24474  insiga  24520  sxbrsigalem0  24621  dya2icobrsiga  24626  sxbrsigalem1  24635  sxbrsigalem2  24636  lgamgulm2  24820  lgamcvglem  24824  erdszelem9  24885  erdsze2lem2  24890  kur14lem9  24900  ptpcon  24920  iinllycon  24941  cvmlift3  25015  imagesset  25798  altxpsspw  25822  axcontlem2  25904  axcontlem10  25912  bpolylem  26094  onsstopbas  26179  onsucconi  26187  onintopsscon  26190  onint1  26199  oninhaus  26200  itg2addnc  26259  itg2gt0cn  26260  ftc1anclem3  26282  ftc1anclem6  26285  ftc1anclem8  26287  topjoin  26394  heiborlem3  26522  eldioph3b  26823  diophin  26831  diophun  26832  eldiophss  26833  fz1ssnn  26871  dsmmsubg  27186  dsmmlss  27187  isnumbasabl  27248  isnumbasgrp  27249  dfacbasgrp  27250  lbslinds  27280  symgtrf  27387  mon1psubm  27502  rrpsscn  27695  stoweidlem34  27759  stirlinglem13  27811  unipwrVD  28944  unipwr  28945  bnj1398  29403  bnj1498  29430  atssbase  30088
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator