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

Theorem ssriv 3348
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 3333 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 ssriv.1 . 2  |-  ( x  e.  A  ->  x  e.  B )
31, 2mpgbir 1598 1  |-  A  C_  B
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  ssid  3363  ssv  3364  difss  3471  ssun1  3507  inss1  3558  0ss  3654  difprsnss  3997  snsspw  4032  uniin  4099  iuniin  4169  iunpwss  4248  pwuni  4511  pwunss  4613  xpsspw  4940  dmin  5034  dmrnssfld  5085  dmcoss  5086  dminss  5239  imainss  5240  fviss  5737  mapsspm  7234  pmsspw  7235  uniixp  7274  pwfilem  7593  dffi3  7669  dfom3  7841  onwf  8025  tcrank  8079  cardprclem  8137  alephsson  8258  ackbij1  8395  cardcf  8409  cfeq0  8413  dfacfin7  8556  hsmexlem6  8588  canthnum  8803  inaprc  8990  nqerf  9086  addnqf  9104  mulnqf  9105  dmrecnq  9124  reclem2pr  9204  wuncn  9324  zssre  10640  zsscn  10641  nnssz  10653  elq  10942  zssq  10947  qssre  10950  rpssre  10988  ixxssixx  11301  iooval2  11320  ioossre  11344  fzssuz  11485  fzssp1  11487  uzdisj  11514  fzossfz  11553  fzouzsplit  11567  fzossnn  11577  fzo0ssnn0  11594  uzrdgfni  11764  seqcoll  12199  wrdexg  12227  wrdexb  12228  fclim  13014  isercolllem3  13127  isercoll  13128  fsumge0  13240  climcnds  13296  divcnv  13298  harmonic  13303  mertenslem1  13326  bitsss  13604  maxprmfct  13781  prminf  13958  prmreclem2  13960  prmreclem3  13961  1arithlem1  13966  1arith  13970  4sqlem19  14006  vdwlem12  14035  restsspw  14352  xpsc0  14480  xpsc1  14481  mremre  14524  mreacs  14578  isfunc  14756  homarel  14886  ledm  15376  lern  15377  prdsgrpd  15643  prdsinvgd  15644  symgtrf  15954  odf1o2  16051  sylow3lem3  16107  sylow3lem6  16110  oppglsm  16120  efgsfo  16215  0frgp  16255  prdscmnd  16322  prdsabld  16323  dprdssv  16479  dprdres  16498  ablfac1b  16544  prdsrngd  16638  prdscrngd  16639  unitss  16685  subrgint  16810  lssintcl  16966  prdslmodd  16971  psrbaglefi  17374  psrbaglefiOLD  17375  coe1mul2lem2  17619  xrge0subm  17697  cnsubmlem  17704  cnsubglem  17705  cnsubdrglem  17707  cnmsubglem  17718  zringlpir  17747  zlpir  17752  zringunit  17755  zrngunit  17756  znf1o  17825  zntoslem  17830  ocvss  17936  dsmmsubg  18009  dsmmlss  18010  lbslinds  18103  cldss2  18475  indiscld  18536  toponmre  18538  iscldtop  18540  1stcfb  18890  llyssnlly  18923  llyidm  18933  nllyidm  18934  toplly  18935  hauslly  18937  lly1stc  18941  1stckgenlem  18967  txindis  19048  pthaus  19052  ptcmpfi  19227  ufinffr  19343  cnflf2  19417  flimfcls  19440  alexsubALTlem3  19462  ptcmplem1  19465  ptcmpg  19470  prdstmdd  19535  prdstgpd  19536  ust0  19635  prdsms  19947  qdensere  20190  blssioo  20213  tgioo  20214  xrtgioo  20224  xrsmopn  20230  zdis  20234  reperflem  20236  xrge0gsumle  20251  xrge0tsms  20252  icopnfhmeo  20356  bndth  20371  ovoliunlem1  20826  ovoliun2  20830  ovolicc2lem4  20844  voliunlem2  20873  voliunlem3  20874  iunmbl  20875  uniioovol  20900  uniioombllem4  20907  vitali  20934  ismbf3d  20973  itg2seq  21061  itg2monolem1  21069  itg2monolem2  21070  itg2monolem3  21071  itg2mono  21072  itg2i1fseqle  21073  itg2i1fseq3  21076  itg2addlem  21077  itg2gt0  21079  itg2cnlem2  21081  limccl  21191  limcresi  21201  dvef  21293  plypf1  21564  aasscn  21668  qssaa  21674  aannenlem1  21678  aannenlem2  21679  aannenlem3  21680  ulmcn  21748  mtestbdd  21754  iblulm  21756  reeff1o  21796  reefgim  21799  efifo  21887  dfrelog  21901  relogf1o  21902  logdmss  21971  logcn  21976  dvloglem  21977  logf1o2  21979  dvlog  21980  dvlog2lem  21981  dvlog2  21982  logtayl  21989  cxpcn  22067  cxpcn2  22068  cxpcn3  22070  resqrcn  22071  efrlim  22247  dfef2  22248  cxp2lim  22254  jensen  22266  wilthlem2  22291  wilthlem3  22292  basellem3  22304  basellem4  22305  prmdvdsfi  22329  vmaval  22335  mumul  22403  sqff1o  22404  musum  22415  fsumvma2  22437  dchrmhm  22464  chtppilim  22608  chto1lb  22611  chpchtlim  22612  chpo1ub  22613  dchrisumlema  22621  dchrmusum2  22627  dchrvmasum2lem  22629  dirith2  22661  mudivsum  22663  mulogsum  22665  mulog2sumlem2  22668  selberg2lem  22683  selberg3lem2  22691  pntrsumo1  22698  pnt2  22746  pnt  22747  axcontlem2  23033  axcontlem10  23041  usgraexmpl  23141  iseupa  23408  phrel  24037  bnrel  24090  hlrel  24113  shex  24436  chsssh  24450  hhssnv  24487  choc1  24552  shunssi  24593  shsleji  24595  shsub1i  24597  shsub2i  24598  shsidmi  24609  omlsii  24628  spanuni  24769  spansni  24782  5oalem7  24885  3oalem3  24889  pjrni  24927  mayete3i  24953  mayete3iOLD  24954  hmopex  25101  cnlnssadj  25306  adjbdln  25309  adjsslnop  25313  shatomistici  25587  hatomistici  25588  xrge0tsmsd  26105  esumpcvgval  26380  hashf2  26386  insiga  26433  sxbrsigalem0  26539  dya2icobrsiga  26544  sxbrsigalem1  26553  sxbrsigalem2  26554  eulerpartlemb  26598  lgamgulm2  26869  lgamcvglem  26873  erdszelem9  26934  erdsze2lem2  26939  kur14lem9  26949  ptpcon  26969  iinllycon  26990  cvmlift3  27064  imagesset  27830  altxpsspw  27854  bpolylem  28037  onsstopbas  28122  onsucconi  28130  onintopsscon  28133  onint1  28142  oninhaus  28143  itg2addnc  28287  itg2gt0cn  28288  ftc1anclem3  28310  ftc1anclem6  28313  ftc1anclem8  28315  topjoin  28427  heiborlem3  28553  eldioph3b  28945  diophin  28953  diophun  28954  eldiophss  28955  fz1ssnn  28991  isnumbasabl  29304  isnumbasgrp  29305  dfacbasgrp  29306  mon1psubm  29416  rrpsscn  29612  stoweidlem34  29672  stirlinglem13  29724  wwlksswrd  30165  wwlksswwlkn  30180  clwlksarewlks  30267  lvecpsslmod  30755  unipwrVD  31267  unipwr  31268  bnj1398  31724  bnj1498  31751  bj-snglss  32043  bj-modabel  32151  atssbase  32505
  Copyright terms: Public domain W3C validator