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

Theorem ssriv 3411
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 3396 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 ssriv.1 . 2  |-  ( x  e.  A  ->  x  e.  B )
31, 2mpgbir 1667 1  |-  A  C_  B
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872    C_ wss 3379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3386  df-ss 3393
This theorem is referenced by:  ssid  3426  ssv  3427  difss  3535  ssun1  3572  inss1  3625  0ss  3736  difprsnss  4078  snsspw  4114  uniin  4182  iuniin  4253  iunpwss  4335  pwuni  4595  pwunss  4701  dmin  5004  dmrnssfld  5055  dmcoss  5056  dminss  5212  imainss  5213  fviss  5883  mapsspm  7460  pmsspw  7461  uniixp  7500  pwfilem  7821  dffi3  7898  dfom3  8105  onwf  8253  tcrank  8307  cardprclem  8365  alephsson  8482  ackbij1  8619  cardcf  8633  cfeq0  8637  dfacfin7  8780  hsmexlem6  8812  canthnum  9025  inaprc  9212  nqerf  9306  addnqf  9324  mulnqf  9325  dmrecnq  9344  reclem2pr  9424  wuncn  9545  zssre  10895  zsscn  10896  nnssz  10908  elq  11217  zssq  11222  qssre  11225  rpssre  11263  ixxssixx  11600  iooval2  11620  ioossre  11647  rge0ssre  11691  fzssz  11752  fz1ssnn  11781  fzssuz  11790  fzssp1  11792  uzdisj  11818  nn0disj  11858  fzossfz  11889  fzouzsplit  11904  fzossnn  11914  fzo0ssnn0  11944  uzrdgfni  12122  seqcoll  12575  wrdexg  12630  wrdexb  12631  fclim  13560  isercolllem3  13673  isercoll  13674  climcnds  13852  divcnv  13854  harmonic  13860  mertenslem1  13883  fprodge0  13990  bpolylem  14044  bitsss  14342  prmssnn  14570  maxprmfct  14595  prminf  14802  prmreclem2  14804  prmreclem3  14805  1arithlem1  14810  1arith  14814  4sqlem19  14856  vdwlem12  14885  restsspw  15273  xpsc0  15409  xpsc1  15410  mremre  15453  mreacs  15507  isfunc  15712  homarel  15874  ledm  16413  lern  16414  sgrpssmgm  16610  mndsssgrp  16611  prdsgrpd  16738  prdsinvgd  16739  symgtrf  17053  odf1o2  17165  sylow3lem3  17224  sylow3lem6  17227  oppglsm  17237  efgsfo  17332  0frgp  17372  prdscmnd  17442  prdsabld  17443  gsummptnn0fz  17558  dprdssv  17592  dprdres  17604  ablfac1b  17646  prdsringd  17783  prdscrngd  17784  unitss  17831  subrgint  17973  lssintcl  18130  prdslmodd  18135  psrbaglefi  18539  coe1mul2lem2  18804  xrge0subm  18952  cnsubmlem  18959  cnsubglem  18960  cnsubdrglem  18962  cnmsubglem  18973  zringlpir  19000  zringlpirOLD  19001  zringunit  19004  znf1o  19064  zntoslem  19069  ocvss  19175  dsmmsubg  19248  dsmmlss  19249  lbslinds  19333  unitg  19924  cldss2  19987  indiscld  20049  toponmre  20051  iscldtop  20053  1stcfb  20402  llyssnlly  20435  llyidm  20445  nllyidm  20446  toplly  20447  hauslly  20449  lly1stc  20453  dissnref  20485  1stckgenlem  20510  txindis  20591  pthaus  20595  ptcmpfi  20770  ufinffr  20886  cnflf2  20960  flimfcls  20983  alexsubALTlem3  21006  ptcmplem1  21009  ptcmpg  21014  prdstmdd  21080  prdstgpd  21081  ust0  21176  prdsms  21488  qdensere  21732  blssioo  21755  tgioo  21756  xrtgioo  21766  xrsmopn  21772  zdis  21776  reperflem  21778  xrge0gsumle  21793  xrge0tsms  21794  icopnfhmeo  21913  bndth  21928  ovoliunlem1  22397  ovoliun2  22401  ovolicc2lem4OLD  22415  ovolicc2lem4  22416  voliunlem2  22446  voliunlem3  22447  uniioovol  22478  uniioombllem4  22486  vitali  22513  ismbf3d  22552  itg2seq  22642  limccl  22772  limcresi  22782  dvef  22874  plypf1  23108  aasscn  23213  qssaa  23222  aannenlem1  23226  aannenlem2  23227  aannenlem3  23228  ulmcn  23296  mtestbdd  23302  iblulm  23304  reeff1o  23344  reefgim  23347  efifo  23438  dfrelog  23457  relogf1o  23458  logdmss  23529  logcn  23534  dvloglem  23535  logf1o2  23537  dvlog  23538  dvlog2lem  23539  dvlog2  23540  logtayl  23547  cxpcn  23627  cxpcn2  23628  cxpcn3  23630  resqrtcn  23631  efrlim  23837  dfef2  23838  cxp2lim  23844  lgamgulm2  23903  lgamcvglem  23907  wilthlem2  23936  wilthlem3  23937  basellem3  23951  basellem4  23952  prmdvdsfi  23976  vmaval  23982  mumul  24050  sqff1o  24051  musum  24062  fsumvma2  24084  dchrmhm  24111  chtppilim  24255  chto1lb  24258  chpchtlim  24259  chpo1ub  24260  dchrisumlema  24268  dchrmusum2  24274  dchrvmasum2lem  24276  dirith2  24308  mudivsum  24310  mulogsum  24312  mulog2sumlem2  24315  selberg2lem  24330  selberg3lem2  24338  pntrsumo1  24345  pnt2  24393  pnt  24394  axcontlem2  24937  usgraexmplef  25070  wwlksswrd  25358  wwlksswwlkn  25373  clwlksarewlks  25429  iseupa  25635  phrel  26398  bnrel  26451  hlrel  26484  shex  26807  chsssh  26820  hhssnv  26857  choc1  26922  shunssi  26963  shsleji  26965  shsub1i  26967  shsub2i  26968  shsidmi  26979  omlsii  26998  spanuni  27139  spansni  27152  5oalem7  27255  3oalem3  27259  pjrni  27297  mayete3i  27323  hmopex  27470  cnlnssadj  27675  adjbdln  27678  adjsslnop  27682  shatomistici  27956  hatomistici  27957  xrge0tsmsd  28500  esumpcvgval  28851  hashf2  28857  insiga  28911  sigapisys  28929  sigaldsys  28933  sigapildsys  28936  sxbrsigalem0  29045  dya2icobrsiga  29050  sxbrsigalem1  29059  sxbrsigalem2  29060  eulerpartlemb  29153  bnj1398  29795  bnj1498  29822  erdszelem9  29874  erdsze2lem2  29879  kur14lem9  29889  ptpcon  29908  iinllycon  29929  cvmlift3  30003  mppsthm  30169  imagesset  30669  altxpsspw  30693  topjoin  30970  onsstopbas  31038  onsucconi  31046  onintopsscon  31049  onint1  31058  oninhaus  31059  bj-snglss  31475  bj-modssabl  31604  icoreunrn  31669  poimirlem8  31855  poimirlem18  31865  poimirlem21  31868  poimirlem22  31869  poimirlem31  31878  poimirlem32  31879  heiborlem3  32052  atssbase  32768  eldioph3b  35519  diophin  35527  diophun  35528  eldiophss  35529  isnumbasabl  35878  isnumbasgrp  35879  dfacbasgrp  35880  mon1psubm  35996  inintabss  36097  intimass  36159  nzin  36580  unipwrVD  37144  unipwr  37145  supxrre3  37445  fsumiunss  37538  rrpsscn  37549  dvnmul  37701  dvnprodlem2  37705  stoweidlem34  37778  stirlinglem13  37831  fourierdlem20  37872  fourierdlem62  37915  fourierdlem83  37936  fourierdlem101  37954  fourierdlem103  37956  fourierdlem104  37957  fourierdlem111  37964  fouriersw  37978  sge0iunmptlemre  38108  nn0ssge0  38117  sge0isum  38120  caragendifcl  38186  carageniuncllem2  38194  hoicvrrex  38225  ringssrng  39481  srhmsubc  39679  srhmsubcALTV  39698  lvecpsslmod  39903  aacllem  40143
  Copyright terms: Public domain W3C validator