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

Theorem ssriv 3197
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 3182 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 ssriv.1 . 2  |-  ( x  e.  A  ->  x  e.  B )
31, 2mpgbir 1540 1  |-  A  C_  B
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696    C_ wss 3165
This theorem is referenced by:  ssid  3210  ssv  3211  difss  3316  ssun1  3351  inss1  3402  0ss  3496  difprsnss  3769  snsspw  3800  uniin  3863  iuniin  3931  iunpwss  4007  pwuni  4222  pwunss  4314  xpsspw  4813  dmin  4902  dmrnssfld  4954  dmcoss  4960  dminss  5111  imainss  5112  fviss  5596  mapsspm  6817  pmsspw  6818  uniixp  6855  pwfilem  7166  dffi3  7200  dfom3  7364  onwf  7518  tcrank  7570  cardprclem  7628  alephsson  7743  ackbij1  7880  cardcf  7894  cfeq0  7898  dfacfin7  8041  hsmexlem6  8073  canthnum  8287  inaprc  8474  nqerf  8570  addnqf  8588  mulnqf  8589  dmrecnq  8608  reclem2pr  8688  wuncn  8808  zssre  10047  zsscn  10048  nnssz  10059  elq  10334  zssq  10339  qssre  10342  rpssre  10380  ixxssixx  10686  iooval2  10705  ioossre  10728  fzssuz  10848  fzssp1  10850  uzdisj  10872  fzossfz  10908  fzouzsplit  10917  uzrdgfni  11037  seqcoll  11417  wrdexg  11441  wrdexb  11465  fclim  12043  isercolllem3  12156  isercoll  12157  fsumge0  12269  climcnds  12326  divcnv  12328  harmonic  12333  mertenslem1  12356  bitsss  12633  maxprmfct  12808  prminf  12978  prmreclem2  12980  prmreclem3  12981  1arithlem1  12986  1arith  12990  4sqlem19  13026  vdwlem12  13055  restsspw  13352  xpsc0  13478  xpsc1  13479  mremre  13522  mreacs  13576  isfunc  13754  homarel  13884  ledm  14362  lern  14363  prdsgrpd  14620  prdsinvgd  14621  odf1o2  14900  sylow3lem3  14956  sylow3lem6  14959  oppglsm  14969  efgsfo  15064  0frgp  15104  prdscmnd  15169  prdsabld  15170  dprdssv  15267  dprdres  15279  ablfac1b  15321  prdsrngd  15411  prdscrngd  15412  unitss  15458  subrgint  15583  lssintcl  15737  prdslmodd  15742  psrbaglefi  16134  coe1mul2lem2  16361  xrge0subm  16428  cnsubmlem  16435  cnsubglem  16436  cnsubdrglem  16438  cnmsubglem  16450  zrngunit  16454  zlpir  16460  znf1o  16521  zntoslem  16526  ocvss  16586  cldss2  16783  indiscld  16844  toponmre  16846  iscldtop  16848  1stcfb  17187  llyssnlly  17220  llyidm  17230  nllyidm  17231  toplly  17232  hauslly  17234  lly1stc  17238  1stckgenlem  17264  txindis  17344  pthaus  17348  ptcmpfi  17520  ufinffr  17640  cnflf2  17714  flimfcls  17737  alexsubALTlem3  17759  ptcmplem1  17762  ptcmpg  17767  prdstmdd  17822  prdstgpd  17823  prdsms  18093  qdensere  18295  blssioo  18317  tgioo  18318  xrtgioo  18328  xrsmopn  18334  zdis  18338  reperflem  18339  xrge0gsumle  18354  xrge0tsms  18355  icopnfhmeo  18457  bndth  18472  ovoliunlem1  18877  ovoliun2  18881  ovolicc2lem4  18895  voliunlem2  18924  voliunlem3  18925  iunmbl  18926  uniioovol  18950  uniioombllem4  18957  vitalilem4  18982  vitali  18984  ismbf3d  19025  itg2seq  19113  itg2monolem1  19121  itg2monolem2  19122  itg2monolem3  19123  itg2mono  19124  itg2i1fseqle  19125  itg2i1fseq3  19128  itg2addlem  19129  itg2gt0  19131  itg2cnlem2  19133  limccl  19241  limcresi  19251  dvef  19343  plypf1  19610  aasscn  19714  qssaa  19720  aannenlem1  19724  aannenlem2  19725  aannenlem3  19726  ulmcn  19792  iblulm  19799  reeff1o  19839  reefgim  19842  efifo  19925  dfrelog  19939  relogf1o  19940  logdmss  20005  logcn  20010  dvloglem  20011  logf1o2  20013  dvlog  20014  dvlog2lem  20015  dvlog2  20016  logtayl  20023  cxpcn  20101  cxpcn2  20102  cxpcn3  20104  resqrcn  20105  efrlim  20280  dfef2  20281  cxp2lim  20287  jensen  20299  wilthlem2  20323  wilthlem3  20324  basellem3  20336  basellem4  20337  prmdvdsfi  20361  vmaval  20367  vmaf  20373  mumul  20435  sqff1o  20436  musum  20447  fsumvma2  20469  dchrmhm  20496  chtppilim  20640  chto1lb  20643  chpchtlim  20644  chpo1ub  20645  dchrisumlema  20653  dchrmusum2  20659  dchrvmasum2lem  20661  dirith2  20693  mudivsum  20695  mulogsum  20697  mulog2sumlem2  20700  selberg2lem  20715  selberg3lem2  20723  pntrsumo1  20730  pnt2  20778  pnt  20779  phrel  21409  bnrel  21462  hlrel  21485  shex  21807  chsssh  21821  hhssnv  21857  choc1  21922  shunssi  21963  shsleji  21965  shsub1i  21967  shsub2i  21968  shsidmi  21979  omlsii  21998  spanuni  22139  spansni  22152  5oalem7  22255  3oalem3  22259  pjrni  22297  mayete3i  22323  mayete3iOLD  22324  hmopex  22471  cnlnssadj  22676  adjbdln  22679  adjsslnop  22683  shatomistici  22957  hatomistici  22958  xrge0tsmsd  23397  esumpcvgval  23461  hashf2  23467  insiga  23513  erdszelem9  23745  erdsze2lem2  23750  kur14lem9  23760  ptpcon  23779  iinllycon  23800  cvmlift3  23874  iseupa  23896  limitssson  24522  altxpsspw  24583  axcontlem2  24665  axcontlem10  24673  bpolylem  24855  onsstopbas  24940  onsucconi  24948  onintopsscon  24951  onint1  24960  oninhaus  24961  itg2gt0cn  25006  tolat  25389  latdir  25398  dmhmph  25636  rnhmph  25637  hst1  25690  topjoin  26417  heiborlem3  26640  eldioph3b  26947  diophin  26955  diophun  26956  eldiophss  26957  fz1ssnn  26995  dsmmsubg  27312  dsmmlss  27313  isnumbasabl  27374  isnumbasgrp  27375  dfacbasgrp  27376  lbslinds  27406  symgtrf  27513  mon1psubm  27628  itgsin0pilem1  27847  stoweidlem34  27886  usgraexmpl  28267  unipwrVD  28924  unipwr  28925  bnj1398  29380  bnj1498  29407  atssbase  30102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator