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

Theorem ssriv 3184
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 3169 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 ssriv.1 . 2  |-  ( x  e.  A  ->  x  e.  B )
31, 2mpgbir 1537 1  |-  A  C_  B
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684    C_ wss 3152
This theorem is referenced by:  ssid  3197  ssv  3198  difss  3303  ssun1  3338  inss1  3389  0ss  3483  difprsn  3756  snsspw  3784  uniin  3847  iuniin  3915  iunpwss  3991  pwuni  4206  pwunss  4298  xpsspw  4797  dmin  4886  dmrnssfld  4938  dmcoss  4944  dminss  5095  imainss  5096  fviss  5580  mapsspm  6801  pmsspw  6802  uniixp  6839  pwfilem  7150  dffi3  7184  dfom3  7348  onwf  7502  tcrank  7554  cardprclem  7612  alephsson  7727  ackbij1  7864  cardcf  7878  cfeq0  7882  dfacfin7  8025  hsmexlem6  8057  canthnum  8271  inaprc  8458  nqerf  8554  addnqf  8572  mulnqf  8573  dmrecnq  8592  reclem2pr  8672  wuncn  8792  zssre  10031  zsscn  10032  nnssz  10043  elq  10318  zssq  10323  qssre  10326  rpssre  10364  ixxssixx  10670  iooval2  10689  ioossre  10712  fzssuz  10832  fzssp1  10834  uzdisj  10856  fzossfz  10892  fzouzsplit  10901  uzrdgfni  11021  seqcoll  11401  wrdexg  11425  wrdexb  11449  fclim  12027  isercolllem3  12140  isercoll  12141  fsumge0  12253  climcnds  12310  divcnv  12312  harmonic  12317  mertenslem1  12340  bitsss  12617  maxprmfct  12792  prminf  12962  prmreclem2  12964  prmreclem3  12965  1arithlem1  12970  1arith  12974  4sqlem19  13010  vdwlem12  13039  restsspw  13336  xpsc0  13462  xpsc1  13463  mremre  13506  mreacs  13560  isfunc  13738  homarel  13868  ledm  14346  lern  14347  prdsgrpd  14604  prdsinvgd  14605  odf1o2  14884  sylow3lem3  14940  sylow3lem6  14943  oppglsm  14953  efgsfo  15048  0frgp  15088  prdscmnd  15153  prdsabld  15154  dprdssv  15251  dprdres  15263  ablfac1b  15305  prdsrngd  15395  prdscrngd  15396  unitss  15442  subrgint  15567  lssintcl  15721  prdslmodd  15726  psrbaglefi  16118  coe1mul2lem2  16345  xrge0subm  16412  cnsubmlem  16419  cnsubglem  16420  cnsubdrglem  16422  cnmsubglem  16434  zrngunit  16438  zlpir  16444  znf1o  16505  zntoslem  16510  ocvss  16570  cldss2  16767  indiscld  16828  toponmre  16830  iscldtop  16832  1stcfb  17171  llyssnlly  17204  llyidm  17214  nllyidm  17215  toplly  17216  hauslly  17218  lly1stc  17222  1stckgenlem  17248  txindis  17328  pthaus  17332  ptcmpfi  17504  ufinffr  17624  cnflf2  17698  flimfcls  17721  alexsubALTlem3  17743  ptcmplem1  17746  ptcmpg  17751  prdstmdd  17806  prdstgpd  17807  prdsms  18077  qdensere  18279  blssioo  18301  tgioo  18302  xrtgioo  18312  xrsmopn  18318  zdis  18322  reperflem  18323  xrge0gsumle  18338  xrge0tsms  18339  icopnfhmeo  18441  bndth  18456  ovoliunlem1  18861  ovoliun2  18865  ovolicc2lem4  18879  voliunlem2  18908  voliunlem3  18909  iunmbl  18910  uniioovol  18934  uniioombllem4  18941  vitalilem4  18966  vitali  18968  ismbf3d  19009  itg2seq  19097  itg2monolem1  19105  itg2monolem2  19106  itg2monolem3  19107  itg2mono  19108  itg2i1fseqle  19109  itg2i1fseq3  19112  itg2addlem  19113  itg2gt0  19115  itg2cnlem2  19117  limccl  19225  limcresi  19235  dvef  19327  plypf1  19594  aasscn  19698  qssaa  19704  aannenlem1  19708  aannenlem2  19709  aannenlem3  19710  ulmcn  19776  iblulm  19783  reeff1o  19823  reefgim  19826  efifo  19909  dfrelog  19923  relogf1o  19924  logdmss  19989  logcn  19994  dvloglem  19995  logf1o2  19997  dvlog  19998  dvlog2lem  19999  dvlog2  20000  logtayl  20007  cxpcn  20085  cxpcn2  20086  cxpcn3  20088  resqrcn  20089  efrlim  20264  dfef2  20265  cxp2lim  20271  jensen  20283  wilthlem2  20307  wilthlem3  20308  basellem3  20320  basellem4  20321  prmdvdsfi  20345  vmaval  20351  vmaf  20357  mumul  20419  sqff1o  20420  musum  20431  fsumvma2  20453  dchrmhm  20480  chtppilim  20624  chto1lb  20627  chpchtlim  20628  chpo1ub  20629  dchrisumlema  20637  dchrmusum2  20643  dchrvmasum2lem  20645  dirith2  20677  mudivsum  20679  mulogsum  20681  mulog2sumlem2  20684  selberg2lem  20699  selberg3lem2  20707  pntrsumo1  20714  pnt2  20762  pnt  20763  phrel  21393  bnrel  21446  hlrel  21469  shex  21791  chsssh  21805  hhssnv  21841  choc1  21906  shunssi  21947  shsleji  21949  shsub1i  21951  shsub2i  21952  shsidmi  21963  omlsii  21982  spanuni  22123  spansni  22136  5oalem7  22239  3oalem3  22243  pjrni  22281  mayete3i  22307  mayete3iOLD  22308  hmopex  22455  cnlnssadj  22660  adjbdln  22663  adjsslnop  22667  shatomistici  22941  hatomistici  22942  xrge0tsmsd  23382  esumpcvgval  23446  hashf2  23452  insiga  23498  erdszelem9  23730  erdsze2lem2  23735  kur14lem9  23745  ptpcon  23764  iinllycon  23785  cvmlift3  23859  iseupa  23881  limitssson  24451  altxpsspw  24511  axcontlem2  24593  axcontlem10  24601  bpolylem  24783  onsstopbas  24868  onsucconi  24876  onintopsscon  24879  onint1  24888  oninhaus  24889  tolat  25286  latdir  25295  dmhmph  25533  rnhmph  25534  hst1  25587  topjoin  26314  heiborlem3  26537  eldioph3b  26844  diophin  26852  diophun  26853  eldiophss  26854  fz1ssnn  26892  dsmmsubg  27209  dsmmlss  27210  isnumbasabl  27271  isnumbasgrp  27272  dfacbasgrp  27273  lbslinds  27303  symgtrf  27410  mon1psubm  27525  itgsin0pilem1  27744  stoweidlem34  27783  usgraexmpl  28133  unipwrVD  28608  unipwr  28609  bnj1398  29064  bnj1498  29091  atssbase  29480
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator