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

Theorem ssriv 3312
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 3297 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 ssriv.1 . 2  |-  ( x  e.  A  ->  x  e.  B )
31, 2mpgbir 1556 1  |-  A  C_  B
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721    C_ wss 3280
This theorem is referenced by:  ssid  3327  ssv  3328  difss  3434  ssun1  3470  inss1  3521  0ss  3616  difprsnss  3894  snsspw  3930  uniin  3995  iuniin  4063  iunpwss  4140  pwuni  4355  pwunss  4448  xpsspw  4945  dmin  5036  dmrnssfld  5088  dmcoss  5094  dminss  5245  imainss  5246  fviss  5743  mapsspm  7006  pmsspw  7007  uniixp  7044  pwfilem  7359  dffi3  7394  dfom3  7558  onwf  7712  tcrank  7764  cardprclem  7822  alephsson  7937  ackbij1  8074  cardcf  8088  cfeq0  8092  dfacfin7  8235  hsmexlem6  8267  canthnum  8480  inaprc  8667  nqerf  8763  addnqf  8781  mulnqf  8782  dmrecnq  8801  reclem2pr  8881  wuncn  9001  zssre  10245  zsscn  10246  nnssz  10257  elq  10532  zssq  10537  qssre  10540  rpssre  10578  ixxssixx  10886  iooval2  10905  ioossre  10928  fzssuz  11049  fzssp1  11051  uzdisj  11074  fzossfz  11112  fzouzsplit  11123  fzossnn  11127  uzrdgfni  11253  seqcoll  11667  wrdexg  11694  wrdexb  11718  fclim  12302  isercolllem3  12415  isercoll  12416  fsumge0  12529  climcnds  12586  divcnv  12588  harmonic  12593  mertenslem1  12616  bitsss  12893  maxprmfct  13068  prminf  13238  prmreclem2  13240  prmreclem3  13241  1arithlem1  13246  1arith  13250  4sqlem19  13286  vdwlem12  13315  restsspw  13614  xpsc0  13740  xpsc1  13741  mremre  13784  mreacs  13838  isfunc  14016  homarel  14146  ledm  14624  lern  14625  prdsgrpd  14882  prdsinvgd  14883  odf1o2  15162  sylow3lem3  15218  sylow3lem6  15221  oppglsm  15231  efgsfo  15326  0frgp  15366  prdscmnd  15431  prdsabld  15432  dprdssv  15529  dprdres  15541  ablfac1b  15583  prdsrngd  15673  prdscrngd  15674  unitss  15720  subrgint  15845  lssintcl  15995  prdslmodd  16000  psrbaglefi  16392  coe1mul2lem2  16616  xrge0subm  16694  cnsubmlem  16701  cnsubglem  16702  cnsubdrglem  16704  cnmsubglem  16716  zrngunit  16720  zlpir  16726  znf1o  16787  zntoslem  16792  ocvss  16852  cldss2  17049  indiscld  17110  toponmre  17112  iscldtop  17114  1stcfb  17461  llyssnlly  17494  llyidm  17504  nllyidm  17505  toplly  17506  hauslly  17508  lly1stc  17512  1stckgenlem  17538  txindis  17619  pthaus  17623  ptcmpfi  17798  ufinffr  17914  cnflf2  17988  flimfcls  18011  alexsubALTlem3  18033  ptcmplem1  18036  ptcmpg  18041  prdstmdd  18106  prdstgpd  18107  ust0  18202  prdsms  18514  qdensere  18757  blssioo  18779  tgioo  18780  xrtgioo  18790  xrsmopn  18796  zdis  18800  reperflem  18802  xrge0gsumle  18817  xrge0tsms  18818  icopnfhmeo  18921  bndth  18936  ovoliunlem1  19351  ovoliun2  19355  ovolicc2lem4  19369  voliunlem2  19398  voliunlem3  19399  iunmbl  19400  uniioovol  19424  uniioombllem4  19431  vitali  19458  ismbf3d  19499  itg2seq  19587  itg2monolem1  19595  itg2monolem2  19596  itg2monolem3  19597  itg2mono  19598  itg2i1fseqle  19599  itg2i1fseq3  19602  itg2addlem  19603  itg2gt0  19605  itg2cnlem2  19607  limccl  19715  limcresi  19725  dvef  19817  plypf1  20084  aasscn  20188  qssaa  20194  aannenlem1  20198  aannenlem2  20199  aannenlem3  20200  ulmcn  20268  mtestbdd  20274  iblulm  20276  reeff1o  20316  reefgim  20319  efifo  20402  dfrelog  20416  relogf1o  20417  logdmss  20486  logcn  20491  dvloglem  20492  logf1o2  20494  dvlog  20495  dvlog2lem  20496  dvlog2  20497  logtayl  20504  cxpcn  20582  cxpcn2  20583  cxpcn3  20585  resqrcn  20586  efrlim  20761  dfef2  20762  cxp2lim  20768  jensen  20780  wilthlem2  20805  wilthlem3  20806  basellem3  20818  basellem4  20819  prmdvdsfi  20843  vmaval  20849  vmaf  20855  mumul  20917  sqff1o  20918  musum  20929  fsumvma2  20951  dchrmhm  20978  chtppilim  21122  chto1lb  21125  chpchtlim  21126  chpo1ub  21127  dchrisumlema  21135  dchrmusum2  21141  dchrvmasum2lem  21143  dirith2  21175  mudivsum  21177  mulogsum  21179  mulog2sumlem2  21182  selberg2lem  21197  selberg3lem2  21205  pntrsumo1  21212  pnt2  21260  pnt  21261  usgraexmpl  21373  iseupa  21640  phrel  22269  bnrel  22322  hlrel  22345  shex  22667  chsssh  22681  hhssnv  22717  choc1  22782  shunssi  22823  shsleji  22825  shsub1i  22827  shsub2i  22828  shsidmi  22839  omlsii  22858  spanuni  22999  spansni  23012  5oalem7  23115  3oalem3  23119  pjrni  23157  mayete3i  23183  mayete3iOLD  23184  hmopex  23331  cnlnssadj  23536  adjbdln  23539  adjsslnop  23543  shatomistici  23817  hatomistici  23818  xrge0tsmsd  24176  esumpcvgval  24421  hashf2  24427  insiga  24473  sxbrsigalem0  24574  dya2icobrsiga  24579  sxbrsigalem1  24588  sxbrsigalem2  24589  lgamgulm2  24773  lgamcvglem  24777  erdszelem9  24838  erdsze2lem2  24843  kur14lem9  24853  ptpcon  24873  iinllycon  24894  cvmlift3  24968  limitssson  25665  altxpsspw  25726  axcontlem2  25808  axcontlem10  25816  bpolylem  25998  onsstopbas  26083  onsucconi  26091  onintopsscon  26094  onint1  26103  oninhaus  26104  itg2addnc  26158  itg2gt0cn  26159  topjoin  26284  heiborlem3  26412  eldioph3b  26713  diophin  26721  diophun  26722  eldiophss  26723  fz1ssnn  26761  dsmmsubg  27077  dsmmlss  27078  isnumbasabl  27139  isnumbasgrp  27140  dfacbasgrp  27141  lbslinds  27171  symgtrf  27278  mon1psubm  27393  rrpsscn  27586  stoweidlem34  27650  stirlinglem13  27702  unipwrVD  28653  unipwr  28654  bnj1398  29109  bnj1498  29136  atssbase  29773
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator