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

Theorem ssriv 3344
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 3329 . 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 3312
This theorem is referenced by:  ssid  3359  ssv  3360  difss  3466  ssun1  3502  inss1  3553  0ss  3648  difprsnss  3926  snsspw  3962  uniin  4027  iuniin  4095  iunpwss  4172  pwuni  4387  pwunss  4480  xpsspw  4977  dmin  5068  dmrnssfld  5120  dmcoss  5126  dminss  5277  imainss  5278  fviss  5775  mapsspm  7038  pmsspw  7039  uniixp  7076  pwfilem  7392  dffi3  7427  dfom3  7591  onwf  7745  tcrank  7797  cardprclem  7855  alephsson  7970  ackbij1  8107  cardcf  8121  cfeq0  8125  dfacfin7  8268  hsmexlem6  8300  canthnum  8513  inaprc  8700  nqerf  8796  addnqf  8814  mulnqf  8815  dmrecnq  8834  reclem2pr  8914  wuncn  9034  zssre  10278  zsscn  10279  nnssz  10290  elq  10565  zssq  10570  qssre  10573  rpssre  10611  ixxssixx  10919  iooval2  10938  ioossre  10961  fzssuz  11082  fzssp1  11084  uzdisj  11107  fzossfz  11145  fzouzsplit  11156  fzossnn  11160  uzrdgfni  11286  seqcoll  11700  wrdexg  11727  wrdexb  11751  fclim  12335  isercolllem3  12448  isercoll  12449  fsumge0  12562  climcnds  12619  divcnv  12621  harmonic  12626  mertenslem1  12649  bitsss  12926  maxprmfct  13101  prminf  13271  prmreclem2  13273  prmreclem3  13274  1arithlem1  13279  1arith  13283  4sqlem19  13319  vdwlem12  13348  restsspw  13647  xpsc0  13773  xpsc1  13774  mremre  13817  mreacs  13871  isfunc  14049  homarel  14179  ledm  14657  lern  14658  prdsgrpd  14915  prdsinvgd  14916  odf1o2  15195  sylow3lem3  15251  sylow3lem6  15254  oppglsm  15264  efgsfo  15359  0frgp  15399  prdscmnd  15464  prdsabld  15465  dprdssv  15562  dprdres  15574  ablfac1b  15616  prdsrngd  15706  prdscrngd  15707  unitss  15753  subrgint  15878  lssintcl  16028  prdslmodd  16033  psrbaglefi  16425  coe1mul2lem2  16649  xrge0subm  16727  cnsubmlem  16734  cnsubglem  16735  cnsubdrglem  16737  cnmsubglem  16749  zrngunit  16753  zlpir  16759  znf1o  16820  zntoslem  16825  ocvss  16885  cldss2  17082  indiscld  17143  toponmre  17145  iscldtop  17147  1stcfb  17496  llyssnlly  17529  llyidm  17539  nllyidm  17540  toplly  17541  hauslly  17543  lly1stc  17547  1stckgenlem  17573  txindis  17654  pthaus  17658  ptcmpfi  17833  ufinffr  17949  cnflf2  18023  flimfcls  18046  alexsubALTlem3  18068  ptcmplem1  18071  ptcmpg  18076  prdstmdd  18141  prdstgpd  18142  ust0  18237  prdsms  18549  qdensere  18792  blssioo  18814  tgioo  18815  xrtgioo  18825  xrsmopn  18831  zdis  18835  reperflem  18837  xrge0gsumle  18852  xrge0tsms  18853  icopnfhmeo  18956  bndth  18971  ovoliunlem1  19386  ovoliun2  19390  ovolicc2lem4  19404  voliunlem2  19433  voliunlem3  19434  iunmbl  19435  uniioovol  19459  uniioombllem4  19466  vitali  19493  ismbf3d  19534  itg2seq  19622  itg2monolem1  19630  itg2monolem2  19631  itg2monolem3  19632  itg2mono  19633  itg2i1fseqle  19634  itg2i1fseq3  19637  itg2addlem  19638  itg2gt0  19640  itg2cnlem2  19642  limccl  19750  limcresi  19760  dvef  19852  plypf1  20119  aasscn  20223  qssaa  20229  aannenlem1  20233  aannenlem2  20234  aannenlem3  20235  ulmcn  20303  mtestbdd  20309  iblulm  20311  reeff1o  20351  reefgim  20354  efifo  20437  dfrelog  20451  relogf1o  20452  logdmss  20521  logcn  20526  dvloglem  20527  logf1o2  20529  dvlog  20530  dvlog2lem  20531  dvlog2  20532  logtayl  20539  cxpcn  20617  cxpcn2  20618  cxpcn3  20620  resqrcn  20621  efrlim  20796  dfef2  20797  cxp2lim  20803  jensen  20815  wilthlem2  20840  wilthlem3  20841  basellem3  20853  basellem4  20854  prmdvdsfi  20878  vmaval  20884  vmaf  20890  mumul  20952  sqff1o  20953  musum  20964  fsumvma2  20986  dchrmhm  21013  chtppilim  21157  chto1lb  21160  chpchtlim  21161  chpo1ub  21162  dchrisumlema  21170  dchrmusum2  21176  dchrvmasum2lem  21178  dirith2  21210  mudivsum  21212  mulogsum  21214  mulog2sumlem2  21217  selberg2lem  21232  selberg3lem2  21240  pntrsumo1  21247  pnt2  21295  pnt  21296  usgraexmpl  21408  iseupa  21675  phrel  22304  bnrel  22357  hlrel  22380  shex  22702  chsssh  22716  hhssnv  22752  choc1  22817  shunssi  22858  shsleji  22860  shsub1i  22862  shsub2i  22863  shsidmi  22874  omlsii  22893  spanuni  23034  spansni  23047  5oalem7  23150  3oalem3  23154  pjrni  23192  mayete3i  23218  mayete3iOLD  23219  hmopex  23366  cnlnssadj  23571  adjbdln  23574  adjsslnop  23578  shatomistici  23852  hatomistici  23853  xrge0tsmsd  24211  esumpcvgval  24456  hashf2  24462  insiga  24508  sxbrsigalem0  24609  dya2icobrsiga  24614  sxbrsigalem1  24623  sxbrsigalem2  24624  lgamgulm2  24808  lgamcvglem  24812  erdszelem9  24873  erdsze2lem2  24878  kur14lem9  24888  ptpcon  24908  iinllycon  24929  cvmlift3  25003  limitssson  25706  imagesset  25748  altxpsspw  25770  axcontlem2  25852  axcontlem10  25860  bpolylem  26042  onsstopbas  26127  onsucconi  26135  onintopsscon  26138  onint1  26147  oninhaus  26148  itg2addnc  26205  itg2gt0cn  26206  topjoin  26331  heiborlem3  26459  eldioph3b  26760  diophin  26768  diophun  26769  eldiophss  26770  fz1ssnn  26808  dsmmsubg  27124  dsmmlss  27125  isnumbasabl  27186  isnumbasgrp  27187  dfacbasgrp  27188  lbslinds  27218  symgtrf  27325  mon1psubm  27440  rrpsscn  27633  stoweidlem34  27697  stirlinglem13  27749  unipwrVD  28798  unipwr  28799  bnj1398  29257  bnj1498  29284  atssbase  29927
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator