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

Theorem ssriv 3467
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 3452 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 ssriv.1 . 2  |-  ( x  e.  A  ->  x  e.  B )
31, 2mpgbir 1596 1  |-  A  C_  B
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758    C_ wss 3435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3442  df-ss 3449
This theorem is referenced by:  ssid  3482  ssv  3483  difss  3590  ssun1  3626  inss1  3677  0ss  3773  difprsnss  4116  snsspw  4151  uniin  4218  iuniin  4288  iunpwss  4367  pwuni  4630  pwunss  4733  xpsspw  5060  dmin  5154  dmrnssfld  5205  dmcoss  5206  dminss  5358  imainss  5359  fviss  5857  mapsspm  7355  pmsspw  7356  uniixp  7395  pwfilem  7715  dffi3  7791  dfom3  7963  onwf  8147  tcrank  8201  cardprclem  8259  alephsson  8380  ackbij1  8517  cardcf  8531  cfeq0  8535  dfacfin7  8678  hsmexlem6  8710  canthnum  8926  inaprc  9113  nqerf  9209  addnqf  9227  mulnqf  9228  dmrecnq  9247  reclem2pr  9327  wuncn  9447  zssre  10763  zsscn  10764  nnssz  10776  elq  11065  zssq  11070  qssre  11073  rpssre  11111  ixxssixx  11424  iooval2  11443  ioossre  11467  rge0ssre  11509  fzssuz  11615  fzssp1  11617  uzdisj  11647  fzossfz  11686  fzouzsplit  11700  fzossnn  11710  fzo0ssnn0  11727  uzrdgfni  11897  seqcoll  12333  wrdexg  12361  wrdexb  12362  fclim  13148  isercolllem3  13261  isercoll  13262  fsumge0  13375  climcnds  13431  divcnv  13433  harmonic  13438  mertenslem1  13461  bitsss  13739  maxprmfct  13916  prminf  14093  prmreclem2  14095  prmreclem3  14096  1arithlem1  14101  1arith  14105  4sqlem19  14141  vdwlem12  14170  restsspw  14488  xpsc0  14616  xpsc1  14617  mremre  14660  mreacs  14714  isfunc  14892  homarel  15022  ledm  15512  lern  15513  prdsgrpd  15782  prdsinvgd  15783  symgtrf  16093  odf1o2  16192  sylow3lem3  16248  sylow3lem6  16251  oppglsm  16261  efgsfo  16356  0frgp  16396  prdscmnd  16463  prdsabld  16464  dprdssv  16627  dprdres  16646  ablfac1b  16692  prdsrngd  16826  prdscrngd  16827  unitss  16874  subrgint  17009  lssintcl  17167  prdslmodd  17172  psrbaglefi  17563  psrbaglefiOLD  17564  coe1mul2lem2  17844  xrge0subm  17978  cnsubmlem  17985  cnsubglem  17986  cnsubdrglem  17988  cnmsubglem  17999  zringlpir  18030  zlpir  18035  zringunit  18038  zrngunit  18039  znf1o  18108  zntoslem  18113  ocvss  18219  dsmmsubg  18292  dsmmlss  18293  lbslinds  18386  cldss2  18765  indiscld  18826  toponmre  18828  iscldtop  18830  1stcfb  19180  llyssnlly  19213  llyidm  19223  nllyidm  19224  toplly  19225  hauslly  19227  lly1stc  19231  1stckgenlem  19257  txindis  19338  pthaus  19342  ptcmpfi  19517  ufinffr  19633  cnflf2  19707  flimfcls  19730  alexsubALTlem3  19752  ptcmplem1  19755  ptcmpg  19760  prdstmdd  19825  prdstgpd  19826  ust0  19925  prdsms  20237  qdensere  20480  blssioo  20503  tgioo  20504  xrtgioo  20514  xrsmopn  20520  zdis  20524  reperflem  20526  xrge0gsumle  20541  xrge0tsms  20542  icopnfhmeo  20646  bndth  20661  ovoliunlem1  21116  ovoliun2  21120  ovolicc2lem4  21134  voliunlem2  21164  voliunlem3  21165  iunmbl  21166  uniioovol  21191  uniioombllem4  21198  vitali  21225  ismbf3d  21264  itg2seq  21352  itg2monolem1  21360  itg2monolem2  21361  itg2monolem3  21362  itg2mono  21363  itg2i1fseqle  21364  itg2i1fseq3  21367  itg2addlem  21368  itg2gt0  21370  itg2cnlem2  21372  limccl  21482  limcresi  21492  dvef  21584  plypf1  21812  aasscn  21916  qssaa  21922  aannenlem1  21926  aannenlem2  21927  aannenlem3  21928  ulmcn  21996  mtestbdd  22002  iblulm  22004  reeff1o  22044  reefgim  22047  efifo  22135  dfrelog  22149  relogf1o  22150  logdmss  22219  logcn  22224  dvloglem  22225  logf1o2  22227  dvlog  22228  dvlog2lem  22229  dvlog2  22230  logtayl  22237  cxpcn  22315  cxpcn2  22316  cxpcn3  22318  resqrcn  22319  efrlim  22495  dfef2  22496  cxp2lim  22502  jensen  22514  wilthlem2  22539  wilthlem3  22540  basellem3  22552  basellem4  22553  prmdvdsfi  22577  vmaval  22583  mumul  22651  sqff1o  22652  musum  22663  fsumvma2  22685  dchrmhm  22712  chtppilim  22856  chto1lb  22859  chpchtlim  22860  chpo1ub  22861  dchrisumlema  22869  dchrmusum2  22875  dchrvmasum2lem  22877  dirith2  22909  mudivsum  22911  mulogsum  22913  mulog2sumlem2  22916  selberg2lem  22931  selberg3lem2  22939  pntrsumo1  22946  pnt2  22994  pnt  22995  axcontlem2  23362  axcontlem10  23370  usgraexmpl  23470  iseupa  23737  phrel  24366  bnrel  24419  hlrel  24442  shex  24765  chsssh  24779  hhssnv  24816  choc1  24881  shunssi  24922  shsleji  24924  shsub1i  24926  shsub2i  24927  shsidmi  24938  omlsii  24957  spanuni  25098  spansni  25111  5oalem7  25214  3oalem3  25218  pjrni  25256  mayete3i  25282  mayete3iOLD  25283  hmopex  25430  cnlnssadj  25635  adjbdln  25638  adjsslnop  25642  shatomistici  25916  hatomistici  25917  xrge0tsmsd  26397  esumpcvgval  26671  hashf2  26677  insiga  26724  sxbrsigalem0  26829  dya2icobrsiga  26834  sxbrsigalem1  26843  sxbrsigalem2  26844  eulerpartlemb  26894  lgamgulm2  27165  lgamcvglem  27169  erdszelem9  27230  erdsze2lem2  27235  kur14lem9  27245  ptpcon  27265  iinllycon  27286  cvmlift3  27360  imagesset  28127  altxpsspw  28151  bpolylem  28334  onsstopbas  28418  onsucconi  28426  onintopsscon  28429  onint1  28438  oninhaus  28439  itg2addnc  28593  itg2gt0cn  28594  ftc1anclem3  28616  ftc1anclem6  28619  ftc1anclem8  28621  topjoin  28733  heiborlem3  28859  eldioph3b  29250  diophin  29258  diophun  29259  eldiophss  29260  fz1ssnn  29296  isnumbasabl  29609  isnumbasgrp  29610  dfacbasgrp  29611  mon1psubm  29721  rrpsscn  29916  stoweidlem34  29976  stirlinglem13  30028  wwlksswrd  30469  wwlksswwlkn  30484  clwlksarewlks  30571  nn0disj  30885  gsummptnn0fz  30957  lvecpsslmod  31167  unipwrVD  31885  unipwr  31886  bnj1398  32342  bnj1498  32369  bj-snglss  32780  bj-modssabl  32901  atssbase  33258
  Copyright terms: Public domain W3C validator