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

Theorem ssriv 3474
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 3459 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 ssriv.1 . 2  |-  ( x  e.  A  ->  x  e.  B )
31, 2mpgbir 1669 1  |-  A  C_  B
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456
This theorem is referenced by:  ssid  3489  ssv  3490  difss  3598  ssun1  3635  inss1  3688  0ss  3797  difprsnss  4138  snsspw  4174  uniin  4242  iuniin  4313  iunpwss  4395  pwuni  4653  pwunss  4759  dmin  5062  dmrnssfld  5113  dmcoss  5114  dminss  5270  imainss  5271  fviss  5939  mapsspm  7513  pmsspw  7514  uniixp  7553  pwfilem  7874  dffi3  7951  dfom3  8152  onwf  8300  tcrank  8354  cardprclem  8412  alephsson  8529  ackbij1  8666  cardcf  8680  cfeq0  8684  dfacfin7  8827  hsmexlem6  8859  canthnum  9073  inaprc  9260  nqerf  9354  addnqf  9372  mulnqf  9373  dmrecnq  9392  reclem2pr  9472  wuncn  9593  zssre  10944  zsscn  10945  nnssz  10957  elq  11266  zssq  11271  qssre  11274  rpssre  11312  ixxssixx  11649  iooval2  11669  ioossre  11696  rge0ssre  11738  fzssz  11799  fz1ssnn  11828  fzssuz  11837  fzssp1  11839  uzdisj  11865  nn0disj  11905  fzossfz  11936  fzouzsplit  11951  fzossnn  11961  fzo0ssnn0  11991  uzrdgfni  12169  seqcoll  12621  wrdexg  12669  wrdexb  12670  fclim  13595  isercolllem3  13708  isercoll  13709  climcnds  13887  divcnv  13889  harmonic  13895  mertenslem1  13918  fprodge0  14025  bpolylem  14079  bitsss  14374  prmssnn  14598  maxprmfct  14623  prminf  14822  prmreclem2  14824  prmreclem3  14825  1arithlem1  14830  1arith  14834  4sqlem19  14876  vdwlem12  14905  restsspw  15289  xpsc0  15417  xpsc1  15418  mremre  15461  mreacs  15515  isfunc  15720  homarel  15882  ledm  16421  lern  16422  sgrpssmgm  16618  mndsssgrp  16619  prdsgrpd  16746  prdsinvgd  16747  symgtrf  17061  odf1o2  17160  sylow3lem3  17216  sylow3lem6  17219  oppglsm  17229  efgsfo  17324  0frgp  17364  prdscmnd  17434  prdsabld  17435  gsummptnn0fz  17550  dprdssv  17584  dprdres  17596  ablfac1b  17638  prdsringd  17775  prdscrngd  17776  unitss  17823  subrgint  17965  lssintcl  18122  prdslmodd  18127  psrbaglefi  18531  coe1mul2lem2  18796  xrge0subm  18944  cnsubmlem  18951  cnsubglem  18952  cnsubdrglem  18954  cnmsubglem  18965  zringlpir  18990  zringunit  18993  znf1o  19053  zntoslem  19058  ocvss  19164  dsmmsubg  19237  dsmmlss  19238  lbslinds  19322  unitg  19913  cldss2  19976  indiscld  20038  toponmre  20040  iscldtop  20042  1stcfb  20391  llyssnlly  20424  llyidm  20434  nllyidm  20435  toplly  20436  hauslly  20438  lly1stc  20442  dissnref  20474  1stckgenlem  20499  txindis  20580  pthaus  20584  ptcmpfi  20759  ufinffr  20875  cnflf2  20949  flimfcls  20972  alexsubALTlem3  20995  ptcmplem1  20998  ptcmpg  21003  prdstmdd  21069  prdstgpd  21070  ust0  21165  prdsms  21477  qdensere  21701  blssioo  21724  tgioo  21725  xrtgioo  21735  xrsmopn  21741  zdis  21745  reperflem  21747  xrge0gsumle  21762  xrge0tsms  21763  icopnfhmeo  21867  bndth  21882  ovoliunlem1  22333  ovoliun2  22337  ovolicc2lem4  22351  voliunlem2  22381  voliunlem3  22382  uniioovol  22413  uniioombllem4  22421  vitali  22448  ismbf3d  22487  itg2seq  22577  limccl  22707  limcresi  22717  dvef  22809  plypf1  23034  aasscn  23139  qssaa  23145  aannenlem1  23149  aannenlem2  23150  aannenlem3  23151  ulmcn  23219  mtestbdd  23225  iblulm  23227  reeff1o  23267  reefgim  23270  efifo  23361  dfrelog  23380  relogf1o  23381  logdmss  23452  logcn  23457  dvloglem  23458  logf1o2  23460  dvlog  23461  dvlog2lem  23462  dvlog2  23463  logtayl  23470  cxpcn  23550  cxpcn2  23551  cxpcn3  23553  resqrtcn  23554  efrlim  23760  dfef2  23761  cxp2lim  23767  lgamgulm2  23826  lgamcvglem  23830  wilthlem2  23859  wilthlem3  23860  basellem3  23872  basellem4  23873  prmdvdsfi  23897  vmaval  23903  mumul  23971  sqff1o  23972  musum  23983  fsumvma2  24005  dchrmhm  24032  chtppilim  24176  chto1lb  24179  chpchtlim  24180  chpo1ub  24181  dchrisumlema  24189  dchrmusum2  24195  dchrvmasum2lem  24197  dirith2  24229  mudivsum  24231  mulogsum  24233  mulog2sumlem2  24236  selberg2lem  24251  selberg3lem2  24259  pntrsumo1  24266  pnt2  24314  pnt  24315  axcontlem2  24841  usgraexmpl  24974  wwlksswrd  25261  wwlksswwlkn  25276  clwlksarewlks  25332  iseupa  25538  phrel  26301  bnrel  26354  hlrel  26377  shex  26700  chsssh  26713  hhssnv  26750  choc1  26815  shunssi  26856  shsleji  26858  shsub1i  26860  shsub2i  26861  shsidmi  26872  omlsii  26891  spanuni  27032  spansni  27045  5oalem7  27148  3oalem3  27152  pjrni  27190  mayete3i  27216  hmopex  27363  cnlnssadj  27568  adjbdln  27571  adjsslnop  27575  shatomistici  27849  hatomistici  27850  xrge0tsmsd  28387  esumpcvgval  28738  hashf2  28744  insiga  28798  sigapisys  28816  sigaldsys  28820  sigapildsys  28823  sxbrsigalem0  28932  dya2icobrsiga  28937  sxbrsigalem1  28946  sxbrsigalem2  28947  eulerpartlemb  29027  bnj1398  29631  bnj1498  29658  erdszelem9  29710  erdsze2lem2  29715  kur14lem9  29725  ptpcon  29744  iinllycon  29765  cvmlift3  29839  mppsthm  30005  imagesset  30505  altxpsspw  30529  topjoin  30806  onsstopbas  30874  onsucconi  30882  onintopsscon  30885  onint1  30894  oninhaus  30895  bj-snglss  31313  bj-modssabl  31442  icoreunrn  31496  poimirlem8  31652  poimirlem18  31662  poimirlem21  31665  poimirlem22  31666  poimirlem31  31675  poimirlem32  31676  heiborlem3  31849  atssbase  32565  eldioph3b  35316  diophin  35324  diophun  35325  eldiophss  35326  isnumbasabl  35671  isnumbasgrp  35672  dfacbasgrp  35673  mon1psubm  35782  intimass  35885  nzin  36304  unipwrVD  36868  unipwr  36869  supxrre3  37157  fsumiunss  37229  rrpsscn  37238  dvnmul  37387  dvnprodlem2  37391  stoweidlem34  37464  stirlinglem13  37517  fourierdlem20  37558  fourierdlem62  37600  fourierdlem83  37621  fourierdlem101  37639  fourierdlem103  37641  fourierdlem104  37642  fourierdlem111  37649  fouriersw  37663  sge0iunmptlemre  37791  caragendifcl  37844  carageniuncllem2  37852  ringssrng  38638  srhmsubc  38836  srhmsubcALTV  38855  lvecpsslmod  39060  aacllem  39301
  Copyright terms: Public domain W3C validator