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

Theorem ssriv 3493
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 3478 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 ssriv.1 . 2  |-  ( x  e.  A  ->  x  e.  B )
31, 2mpgbir 1627 1  |-  A  C_  B
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  ssid  3508  ssv  3509  difss  3617  ssun1  3653  inss1  3704  0ss  3813  difprsnss  4151  snsspw  4187  uniin  4255  iuniin  4326  iunpwss  4408  pwuni  4668  pwunss  4774  xpsspw  5104  dmin  5199  dmrnssfld  5250  dmcoss  5251  dminss  5405  imainss  5406  fviss  5906  mapsspm  7445  pmsspw  7446  uniixp  7485  pwfilem  7806  dffi3  7883  dfom3  8055  onwf  8239  tcrank  8293  cardprclem  8351  alephsson  8472  ackbij1  8609  cardcf  8623  cfeq0  8627  dfacfin7  8770  hsmexlem6  8802  canthnum  9016  inaprc  9203  nqerf  9297  addnqf  9315  mulnqf  9316  dmrecnq  9335  reclem2pr  9415  wuncn  9536  zssre  10867  zsscn  10868  nnssz  10880  elq  11185  zssq  11190  qssre  11193  rpssre  11231  ixxssixx  11546  iooval2  11565  ioossre  11589  rge0ssre  11631  fz1ssnn  11719  fzssuz  11728  fzssp1  11730  uzdisj  11755  nn0disj  11795  fzossfz  11822  fzouzsplit  11837  fzossnn  11847  fzo0ssnn0  11877  uzrdgfni  12051  seqcoll  12496  wrdexg  12544  wrdexb  12545  fclim  13458  isercolllem3  13571  isercoll  13572  climcnds  13745  divcnv  13747  harmonic  13752  mertenslem1  13775  bitsss  14160  maxprmfct  14338  prminf  14517  prmreclem2  14519  prmreclem3  14520  1arithlem1  14525  1arith  14529  4sqlem19  14565  vdwlem12  14594  restsspw  14921  xpsc0  15049  xpsc1  15050  mremre  15093  mreacs  15147  isfunc  15352  homarel  15514  ledm  16053  lern  16054  sgrpssmgm  16250  mndsssgrp  16251  prdsgrpd  16378  prdsinvgd  16379  symgtrf  16693  odf1o2  16792  sylow3lem3  16848  sylow3lem6  16851  oppglsm  16861  efgsfo  16956  0frgp  16996  prdscmnd  17066  prdsabld  17067  gsummptnn0fz  17209  dprdssv  17251  dprdres  17270  ablfac1b  17316  prdsringd  17456  prdscrngd  17457  unitss  17504  subrgint  17646  lssintcl  17805  prdslmodd  17810  psrbaglefi  18218  psrbaglefiOLD  18219  coe1mul2lem2  18504  xrge0subm  18654  cnsubmlem  18661  cnsubglem  18662  cnsubdrglem  18664  cnmsubglem  18675  zringlpir  18700  zringunit  18703  znf1o  18763  zntoslem  18768  ocvss  18874  dsmmsubg  18947  dsmmlss  18948  lbslinds  19035  unitg  19635  cldss2  19698  indiscld  19759  toponmre  19761  iscldtop  19763  1stcfb  20112  llyssnlly  20145  llyidm  20155  nllyidm  20156  toplly  20157  hauslly  20159  lly1stc  20163  dissnref  20195  1stckgenlem  20220  txindis  20301  pthaus  20305  ptcmpfi  20480  ufinffr  20596  cnflf2  20670  flimfcls  20693  alexsubALTlem3  20715  ptcmplem1  20718  ptcmpg  20723  prdstmdd  20788  prdstgpd  20789  ust0  20888  prdsms  21200  qdensere  21443  blssioo  21466  tgioo  21467  xrtgioo  21477  xrsmopn  21483  zdis  21487  reperflem  21489  xrge0gsumle  21504  xrge0tsms  21505  icopnfhmeo  21609  bndth  21624  ovoliunlem1  22079  ovoliun2  22083  ovolicc2lem4  22097  voliunlem2  22127  voliunlem3  22128  uniioovol  22154  uniioombllem4  22161  vitali  22188  ismbf3d  22227  itg2seq  22315  limccl  22445  limcresi  22455  dvef  22547  plypf1  22775  aasscn  22880  qssaa  22886  aannenlem1  22890  aannenlem2  22891  aannenlem3  22892  ulmcn  22960  mtestbdd  22966  iblulm  22968  reeff1o  23008  reefgim  23011  efifo  23100  dfrelog  23119  relogf1o  23120  logdmss  23191  logcn  23196  dvloglem  23197  logf1o2  23199  dvlog  23200  dvlog2lem  23201  dvlog2  23202  logtayl  23209  cxpcn  23287  cxpcn2  23288  cxpcn3  23290  resqrtcn  23291  efrlim  23497  dfef2  23498  cxp2lim  23504  wilthlem2  23541  wilthlem3  23542  basellem3  23554  basellem4  23555  prmdvdsfi  23579  vmaval  23585  mumul  23653  sqff1o  23654  musum  23665  fsumvma2  23687  dchrmhm  23714  chtppilim  23858  chto1lb  23861  chpchtlim  23862  chpo1ub  23863  dchrisumlema  23871  dchrmusum2  23877  dchrvmasum2lem  23879  dirith2  23911  mudivsum  23913  mulogsum  23915  mulog2sumlem2  23918  selberg2lem  23933  selberg3lem2  23941  pntrsumo1  23948  pnt2  23996  pnt  23997  axcontlem2  24470  usgraexmpl  24603  wwlksswrd  24890  wwlksswwlkn  24905  clwlksarewlks  24961  iseupa  25167  phrel  25928  bnrel  25981  hlrel  26004  shex  26327  chsssh  26341  hhssnv  26378  choc1  26443  shunssi  26484  shsleji  26486  shsub1i  26488  shsub2i  26489  shsidmi  26500  omlsii  26519  spanuni  26660  spansni  26673  5oalem7  26776  3oalem3  26780  pjrni  26818  mayete3i  26844  mayete3iOLD  26845  hmopex  26992  cnlnssadj  27197  adjbdln  27200  adjsslnop  27204  shatomistici  27478  hatomistici  27479  xrge0tsmsd  28010  esumpcvgval  28307  hashf2  28313  insiga  28367  sigapisys  28384  sigaldsys  28386  sigapildsys  28388  sxbrsigalem0  28479  dya2icobrsiga  28484  sxbrsigalem1  28493  sxbrsigalem2  28494  eulerpartlemb  28571  lgamgulm2  28842  lgamcvglem  28846  erdszelem9  28907  erdsze2lem2  28912  kur14lem9  28922  ptpcon  28942  iinllycon  28963  cvmlift3  29037  mppsthm  29203  imagesset  29831  altxpsspw  29855  bpolylem  30038  onsstopbas  30122  onsucconi  30130  onintopsscon  30133  onint1  30142  oninhaus  30143  topjoin  30423  heiborlem3  30549  eldioph3b  30937  diophin  30945  diophun  30946  eldiophss  30947  isnumbasabl  31296  isnumbasgrp  31297  dfacbasgrp  31298  mon1psubm  31407  nzin  31464  fzssz  31706  rrpsscn  31821  fprodge0  31836  dvnmul  31979  dvnprodlem2  31983  stoweidlem34  32055  stirlinglem13  32107  fourierdlem20  32148  fourierdlem62  32190  fourierdlem83  32211  fourierdlem101  32229  fourierdlem103  32231  fourierdlem104  32232  fourierdlem111  32239  fouriersw  32253  ringssrng  32940  srhmsubc  33138  srhmsubcALTV  33157  lvecpsslmod  33362  aacllem  33604  unipwrVD  34032  unipwr  34033  bnj1398  34491  bnj1498  34518  bj-snglss  34929  bj-modssabl  35058  atssbase  35412  intimass  38180
  Copyright terms: Public domain W3C validator