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

Theorem ssriv 3355
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 3340 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 ssriv.1 . 2  |-  ( x  e.  A  ->  x  e.  B )
31, 2mpgbir 1595 1  |-  A  C_  B
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337
This theorem is referenced by:  ssid  3370  ssv  3371  difss  3478  ssun1  3514  inss1  3565  0ss  3661  difprsnss  4004  snsspw  4039  uniin  4106  iuniin  4176  iunpwss  4255  pwuni  4518  pwunss  4621  xpsspw  4948  dmin  5042  dmrnssfld  5093  dmcoss  5094  dminss  5246  imainss  5247  fviss  5744  mapsspm  7238  pmsspw  7239  uniixp  7278  pwfilem  7597  dffi3  7673  dfom3  7845  onwf  8029  tcrank  8083  cardprclem  8141  alephsson  8262  ackbij1  8399  cardcf  8413  cfeq0  8417  dfacfin7  8560  hsmexlem6  8592  canthnum  8808  inaprc  8995  nqerf  9091  addnqf  9109  mulnqf  9110  dmrecnq  9129  reclem2pr  9209  wuncn  9329  zssre  10645  zsscn  10646  nnssz  10658  elq  10947  zssq  10952  qssre  10955  rpssre  10993  ixxssixx  11306  iooval2  11325  ioossre  11349  rge0ssre  11385  fzssuz  11491  fzssp1  11493  uzdisj  11523  fzossfz  11562  fzouzsplit  11576  fzossnn  11586  fzo0ssnn0  11603  uzrdgfni  11773  seqcoll  12208  wrdexg  12236  wrdexb  12237  fclim  13023  isercolllem3  13136  isercoll  13137  fsumge0  13250  climcnds  13306  divcnv  13308  harmonic  13313  mertenslem1  13336  bitsss  13614  maxprmfct  13791  prminf  13968  prmreclem2  13970  prmreclem3  13971  1arithlem1  13976  1arith  13980  4sqlem19  14016  vdwlem12  14045  restsspw  14362  xpsc0  14490  xpsc1  14491  mremre  14534  mreacs  14588  isfunc  14766  homarel  14896  ledm  15386  lern  15387  prdsgrpd  15655  prdsinvgd  15656  symgtrf  15966  odf1o2  16063  sylow3lem3  16119  sylow3lem6  16122  oppglsm  16132  efgsfo  16227  0frgp  16267  prdscmnd  16334  prdsabld  16335  dprdssv  16496  dprdres  16515  ablfac1b  16561  prdsrngd  16694  prdscrngd  16695  unitss  16742  subrgint  16867  lssintcl  17025  prdslmodd  17030  psrbaglefi  17421  psrbaglefiOLD  17422  coe1mul2lem2  17702  xrge0subm  17834  cnsubmlem  17841  cnsubglem  17842  cnsubdrglem  17844  cnmsubglem  17855  zringlpir  17886  zlpir  17891  zringunit  17894  zrngunit  17895  znf1o  17964  zntoslem  17969  ocvss  18075  dsmmsubg  18148  dsmmlss  18149  lbslinds  18242  cldss2  18614  indiscld  18675  toponmre  18677  iscldtop  18679  1stcfb  19029  llyssnlly  19062  llyidm  19072  nllyidm  19073  toplly  19074  hauslly  19076  lly1stc  19080  1stckgenlem  19106  txindis  19187  pthaus  19191  ptcmpfi  19366  ufinffr  19482  cnflf2  19556  flimfcls  19579  alexsubALTlem3  19601  ptcmplem1  19604  ptcmpg  19609  prdstmdd  19674  prdstgpd  19675  ust0  19774  prdsms  20086  qdensere  20329  blssioo  20352  tgioo  20353  xrtgioo  20363  xrsmopn  20369  zdis  20373  reperflem  20375  xrge0gsumle  20390  xrge0tsms  20391  icopnfhmeo  20495  bndth  20510  ovoliunlem1  20965  ovoliun2  20969  ovolicc2lem4  20983  voliunlem2  21012  voliunlem3  21013  iunmbl  21014  uniioovol  21039  uniioombllem4  21046  vitali  21073  ismbf3d  21112  itg2seq  21200  itg2monolem1  21208  itg2monolem2  21209  itg2monolem3  21210  itg2mono  21211  itg2i1fseqle  21212  itg2i1fseq3  21215  itg2addlem  21216  itg2gt0  21218  itg2cnlem2  21220  limccl  21330  limcresi  21340  dvef  21432  plypf1  21660  aasscn  21764  qssaa  21770  aannenlem1  21774  aannenlem2  21775  aannenlem3  21776  ulmcn  21844  mtestbdd  21850  iblulm  21852  reeff1o  21892  reefgim  21895  efifo  21983  dfrelog  21997  relogf1o  21998  logdmss  22067  logcn  22072  dvloglem  22073  logf1o2  22075  dvlog  22076  dvlog2lem  22077  dvlog2  22078  logtayl  22085  cxpcn  22163  cxpcn2  22164  cxpcn3  22166  resqrcn  22167  efrlim  22343  dfef2  22344  cxp2lim  22350  jensen  22362  wilthlem2  22387  wilthlem3  22388  basellem3  22400  basellem4  22401  prmdvdsfi  22425  vmaval  22431  mumul  22499  sqff1o  22500  musum  22511  fsumvma2  22533  dchrmhm  22560  chtppilim  22704  chto1lb  22707  chpchtlim  22708  chpo1ub  22709  dchrisumlema  22717  dchrmusum2  22723  dchrvmasum2lem  22725  dirith2  22757  mudivsum  22759  mulogsum  22761  mulog2sumlem2  22764  selberg2lem  22779  selberg3lem2  22787  pntrsumo1  22794  pnt2  22842  pnt  22843  axcontlem2  23179  axcontlem10  23187  usgraexmpl  23287  iseupa  23554  phrel  24183  bnrel  24236  hlrel  24259  shex  24582  chsssh  24596  hhssnv  24633  choc1  24698  shunssi  24739  shsleji  24741  shsub1i  24743  shsub2i  24744  shsidmi  24755  omlsii  24774  spanuni  24915  spansni  24928  5oalem7  25031  3oalem3  25035  pjrni  25073  mayete3i  25099  mayete3iOLD  25100  hmopex  25247  cnlnssadj  25452  adjbdln  25455  adjsslnop  25459  shatomistici  25733  hatomistici  25734  xrge0tsmsd  26221  esumpcvgval  26496  hashf2  26502  insiga  26549  sxbrsigalem0  26655  dya2icobrsiga  26660  sxbrsigalem1  26669  sxbrsigalem2  26670  eulerpartlemb  26720  lgamgulm2  26991  lgamcvglem  26995  erdszelem9  27056  erdsze2lem2  27061  kur14lem9  27071  ptpcon  27091  iinllycon  27112  cvmlift3  27186  imagesset  27953  altxpsspw  27977  bpolylem  28160  onsstopbas  28245  onsucconi  28253  onintopsscon  28256  onint1  28265  oninhaus  28266  itg2addnc  28417  itg2gt0cn  28418  ftc1anclem3  28440  ftc1anclem6  28443  ftc1anclem8  28445  topjoin  28557  heiborlem3  28683  eldioph3b  29074  diophin  29082  diophun  29083  eldiophss  29084  fz1ssnn  29120  isnumbasabl  29433  isnumbasgrp  29434  dfacbasgrp  29435  mon1psubm  29545  rrpsscn  29740  stoweidlem34  29800  stirlinglem13  29852  wwlksswrd  30293  wwlksswwlkn  30308  clwlksarewlks  30395  gsummptnn0fz  30775  lvecpsslmod  30980  unipwrVD  31497  unipwr  31498  bnj1398  31954  bnj1498  31981  bj-snglss  32363  bj-modabel  32474  atssbase  32828
  Copyright terms: Public domain W3C validator