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

Theorem ssriv 3448
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 3433 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 ssriv.1 . 2  |-  ( x  e.  A  ->  x  e.  B )
31, 2mpgbir 1684 1  |-  A  C_  B
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430
This theorem is referenced by:  ssid  3463  ssv  3464  difss  3572  ssun1  3609  inss1  3664  0ss  3775  difprsnss  4120  snsspw  4156  uniin  4232  iuniin  4303  iunpwss  4385  pwuni  4645  pwunss  4758  dmin  5061  dmrnssfld  5112  dmcoss  5113  dminss  5269  imainss  5270  fviss  5946  mapsspm  7531  pmsspw  7532  uniixp  7571  pwfilem  7894  dffi3  7971  dfom3  8178  onwf  8327  tcrank  8381  cardprclem  8439  alephsson  8557  ackbij1  8694  cardcf  8708  cfeq0  8712  dfacfin7  8855  hsmexlem6  8887  canthnum  9100  inaprc  9287  nqerf  9381  addnqf  9399  mulnqf  9400  dmrecnq  9419  reclem2pr  9499  wuncn  9620  zssre  10973  zsscn  10974  nnssz  10986  elq  11295  zssq  11300  qssre  11303  rpssre  11341  ixxssixx  11678  iooval2  11698  ioossre  11725  rge0ssre  11769  fzssz  11830  fz1ssnn  11859  fzssuz  11868  fzssp1  11870  uzdisj  11896  nn0disj  11937  fzossfz  11969  fzouzsplit  11984  fzossnn  11995  fzo0ssnn0  12025  uzrdgfni  12204  seqcoll  12660  wrdexg  12715  wrdexb  12716  fclim  13666  isercolllem3  13779  isercoll  13780  climcnds  13958  divcnv  13960  harmonic  13966  mertenslem1  13989  fprodge0  14096  bpolylem  14150  bitsss  14448  prmssnn  14676  maxprmfct  14701  prminf  14908  prmreclem2  14910  prmreclem3  14911  1arithlem1  14916  1arith  14920  4sqlem19  14962  vdwlem12  14991  restsspw  15379  xpsc0  15515  xpsc1  15516  mremre  15559  mreacs  15613  isfunc  15818  homarel  15980  ledm  16519  lern  16520  sgrpssmgm  16716  mndsssgrp  16717  prdsgrpd  16844  prdsinvgd  16845  symgtrf  17159  odf1o2  17271  sylow3lem3  17330  sylow3lem6  17333  oppglsm  17343  efgsfo  17438  0frgp  17478  prdscmnd  17548  prdsabld  17549  gsummptnn0fz  17664  dprdssv  17698  dprdres  17710  ablfac1b  17752  prdsringd  17889  prdscrngd  17890  unitss  17937  subrgint  18079  lssintcl  18236  prdslmodd  18241  psrbaglefi  18645  coe1mul2lem2  18910  xrge0subm  19058  cnsubmlem  19065  cnsubglem  19066  cnsubdrglem  19068  cnmsubglem  19079  zringlpir  19107  zringlpirOLD  19108  zringunit  19111  znf1o  19171  zntoslem  19176  ocvss  19282  dsmmsubg  19355  dsmmlss  19356  lbslinds  19440  unitg  20031  cldss2  20094  indiscld  20156  toponmre  20158  iscldtop  20160  1stcfb  20509  llyssnlly  20542  llyidm  20552  nllyidm  20553  toplly  20554  hauslly  20556  lly1stc  20560  dissnref  20592  1stckgenlem  20617  txindis  20698  pthaus  20702  ptcmpfi  20877  ufinffr  20993  cnflf2  21067  flimfcls  21090  alexsubALTlem3  21113  ptcmplem1  21116  ptcmpg  21121  prdstmdd  21187  prdstgpd  21188  ust0  21283  prdsms  21595  qdensere  21839  blssioo  21862  tgioo  21863  xrtgioo  21873  xrsmopn  21879  zdis  21883  reperflem  21885  xrge0gsumle  21900  xrge0tsms  21901  icopnfhmeo  22020  bndth  22035  ovoliunlem1  22504  ovoliun2  22508  ovolicc2lem4OLD  22522  ovolicc2lem4  22523  voliunlem2  22553  voliunlem3  22554  uniioovol  22585  uniioombllem4  22593  vitali  22620  ismbf3d  22659  itg2seq  22749  limccl  22879  limcresi  22889  dvef  22981  plypf1  23215  aasscn  23320  qssaa  23329  aannenlem1  23333  aannenlem2  23334  aannenlem3  23335  ulmcn  23403  mtestbdd  23409  iblulm  23411  reeff1o  23451  reefgim  23454  efifo  23545  dfrelog  23564  relogf1o  23565  logdmss  23636  logcn  23641  dvloglem  23642  logf1o2  23644  dvlog  23645  dvlog2lem  23646  dvlog2  23647  logtayl  23654  cxpcn  23734  cxpcn2  23735  cxpcn3  23737  resqrtcn  23738  efrlim  23944  dfef2  23945  cxp2lim  23951  lgamgulm2  24010  lgamcvglem  24014  wilthlem2  24043  wilthlem3  24044  basellem3  24058  basellem4  24059  prmdvdsfi  24083  vmaval  24089  mumul  24157  sqff1o  24158  musum  24169  fsumvma2  24191  dchrmhm  24218  chtppilim  24362  chto1lb  24365  chpchtlim  24366  chpo1ub  24367  dchrisumlema  24375  dchrmusum2  24381  dchrvmasum2lem  24383  dirith2  24415  mudivsum  24417  mulogsum  24419  mulog2sumlem2  24422  selberg2lem  24437  selberg3lem2  24445  pntrsumo1  24452  pnt2  24500  pnt  24501  axcontlem2  25044  usgraexmplef  25177  wwlksswrd  25465  wwlksswwlkn  25480  clwlksarewlks  25536  iseupa  25742  phrel  26505  bnrel  26558  hlrel  26591  shex  26914  chsssh  26927  hhssnv  26964  choc1  27029  shunssi  27070  shsleji  27072  shsub1i  27074  shsub2i  27075  shsidmi  27086  omlsii  27105  spanuni  27246  spansni  27259  5oalem7  27362  3oalem3  27366  pjrni  27404  mayete3i  27430  hmopex  27577  cnlnssadj  27782  adjbdln  27785  adjsslnop  27789  shatomistici  28063  hatomistici  28064  xrge0tsmsd  28597  esumpcvgval  28948  hashf2  28954  insiga  29008  sigapisys  29026  sigaldsys  29030  sigapildsys  29033  sxbrsigalem0  29142  dya2icobrsiga  29147  sxbrsigalem1  29156  sxbrsigalem2  29157  eulerpartlemb  29250  bnj1398  29892  bnj1498  29919  erdszelem9  29971  erdsze2lem2  29976  kur14lem9  29986  ptpcon  30005  iinllycon  30026  cvmlift3  30100  mppsthm  30266  imagesset  30769  altxpsspw  30793  topjoin  31070  onsstopbas  31138  onsucconi  31146  onintopsscon  31149  onint1  31158  oninhaus  31159  bj-snglss  31609  bj-modssabl  31742  icoreunrn  31807  poimirlem8  31993  poimirlem18  32003  poimirlem21  32006  poimirlem22  32007  poimirlem31  32016  poimirlem32  32017  heiborlem3  32190  atssbase  32901  eldioph3b  35652  diophin  35660  diophun  35661  eldiophss  35662  isnumbasabl  36010  isnumbasgrp  36011  dfacbasgrp  36012  mon1psubm  36128  inintabss  36229  intimass  36291  nzin  36711  unipwrVD  37268  unipwr  37269  supxrre3  37586  fsumiunss  37692  rrpsscn  37704  dvnmul  37856  dvnprodlem2  37860  stoweidlem34  37933  stirlinglem13  37986  fourierdlem20  38027  fourierdlem62  38070  fourierdlem83  38091  fourierdlem101  38109  fourierdlem103  38111  fourierdlem104  38112  fourierdlem111  38119  fouriersw  38133  qndenserrnbllem  38201  sge0iunmptlemre  38295  nn0ssge0  38304  sge0isum  38307  caragendifcl  38373  carageniuncllem2  38381  hoicvrrex  38416  griedg0ssusgr  39387  uvtxassvtx  39512  rgrusgrprc  39654  clwlks1wlks  39803  ringssrng  40153  srhmsubc  40351  srhmsubcALTV  40370  lvecpsslmod  40573  aacllem  40813
  Copyright terms: Public domain W3C validator