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 1609 1  |-  A  C_  B
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475
This theorem is referenced by:  ssid  3508  ssv  3509  difss  3616  ssun1  3652  inss1  3703  0ss  3800  difprsnss  4150  snsspw  4186  uniin  4254  iuniin  4326  iunpwss  4405  pwuni  4668  pwunss  4775  xpsspw  5106  dmin  5200  dmrnssfld  5251  dmcoss  5252  dminss  5410  imainss  5411  fviss  5916  mapsspm  7454  pmsspw  7455  uniixp  7494  pwfilem  7816  dffi3  7893  dfom3  8067  onwf  8251  tcrank  8305  cardprclem  8363  alephsson  8484  ackbij1  8621  cardcf  8635  cfeq0  8639  dfacfin7  8782  hsmexlem6  8814  canthnum  9030  inaprc  9217  nqerf  9311  addnqf  9329  mulnqf  9330  dmrecnq  9349  reclem2pr  9429  wuncn  9550  zssre  10877  zsscn  10878  nnssz  10890  elq  11193  zssq  11198  qssre  11201  rpssre  11239  ixxssixx  11552  iooval2  11571  ioossre  11595  rge0ssre  11637  fzssuz  11733  fzssp1  11735  uzdisj  11760  nn0disj  11799  fzossfz  11825  fzouzsplit  11839  fzossnn  11849  fzo0ssnn0  11875  uzrdgfni  12048  seqcoll  12491  wrdexg  12536  wrdexb  12537  fclim  13355  isercolllem3  13468  isercoll  13469  climcnds  13642  divcnv  13644  harmonic  13649  mertenslem1  13672  bitsss  13953  maxprmfct  14131  prminf  14310  prmreclem2  14312  prmreclem3  14313  1arithlem1  14318  1arith  14322  4sqlem19  14358  vdwlem12  14387  restsspw  14706  xpsc0  14834  xpsc1  14835  mremre  14878  mreacs  14932  isfunc  15107  homarel  15237  ledm  15728  lern  15729  sgrpssmgm  15925  mndsssgrp  15926  prdsgrpd  16053  prdsinvgd  16054  symgtrf  16368  odf1o2  16467  sylow3lem3  16523  sylow3lem6  16526  oppglsm  16536  efgsfo  16631  0frgp  16671  prdscmnd  16741  prdsabld  16742  gsummptnn0fz  16888  dprdssv  16930  dprdres  16949  ablfac1b  16995  prdsringd  17135  prdscrngd  17136  unitss  17183  subrgint  17325  lssintcl  17484  prdslmodd  17489  psrbaglefi  17897  psrbaglefiOLD  17898  coe1mul2lem2  18183  xrge0subm  18333  cnsubmlem  18340  cnsubglem  18341  cnsubdrglem  18343  cnmsubglem  18354  zringlpir  18385  zlpir  18390  zringunit  18393  zrngunit  18394  znf1o  18463  zntoslem  18468  ocvss  18574  dsmmsubg  18647  dsmmlss  18648  lbslinds  18741  unitg  19341  cldss2  19404  indiscld  19465  toponmre  19467  iscldtop  19469  1stcfb  19819  llyssnlly  19852  llyidm  19862  nllyidm  19863  toplly  19864  hauslly  19866  lly1stc  19870  dissnref  19902  1stckgenlem  19927  txindis  20008  pthaus  20012  ptcmpfi  20187  ufinffr  20303  cnflf2  20377  flimfcls  20400  alexsubALTlem3  20422  ptcmplem1  20425  ptcmpg  20430  prdstmdd  20495  prdstgpd  20496  ust0  20595  prdsms  20907  qdensere  21150  blssioo  21173  tgioo  21174  xrtgioo  21184  xrsmopn  21190  zdis  21194  reperflem  21196  xrge0gsumle  21211  xrge0tsms  21212  icopnfhmeo  21316  bndth  21331  ovoliunlem1  21786  ovoliun2  21790  ovolicc2lem4  21804  voliunlem2  21834  voliunlem3  21835  uniioovol  21861  uniioombllem4  21868  vitali  21895  ismbf3d  21934  itg2seq  22022  limccl  22152  limcresi  22162  dvef  22254  plypf1  22482  aasscn  22586  qssaa  22592  aannenlem1  22596  aannenlem2  22597  aannenlem3  22598  ulmcn  22666  mtestbdd  22672  iblulm  22674  reeff1o  22714  reefgim  22717  efifo  22806  dfrelog  22825  relogf1o  22826  logdmss  22895  logcn  22900  dvloglem  22901  logf1o2  22903  dvlog  22904  dvlog2lem  22905  dvlog2  22906  logtayl  22913  cxpcn  22991  cxpcn2  22992  cxpcn3  22994  resqrtcn  22995  efrlim  23171  dfef2  23172  cxp2lim  23178  wilthlem2  23215  wilthlem3  23216  basellem3  23228  basellem4  23229  prmdvdsfi  23253  vmaval  23259  mumul  23327  sqff1o  23328  musum  23339  fsumvma2  23361  dchrmhm  23388  chtppilim  23532  chto1lb  23535  chpchtlim  23536  chpo1ub  23537  dchrisumlema  23545  dchrmusum2  23551  dchrvmasum2lem  23553  dirith2  23585  mudivsum  23587  mulogsum  23589  mulog2sumlem2  23592  selberg2lem  23607  selberg3lem2  23615  pntrsumo1  23622  pnt2  23670  pnt  23671  axcontlem2  24140  usgraexmpl  24273  wwlksswrd  24560  wwlksswwlkn  24575  clwlksarewlks  24631  iseupa  24837  phrel  25602  bnrel  25655  hlrel  25678  shex  26001  chsssh  26015  hhssnv  26052  choc1  26117  shunssi  26158  shsleji  26160  shsub1i  26162  shsub2i  26163  shsidmi  26174  omlsii  26193  spanuni  26334  spansni  26347  5oalem7  26450  3oalem3  26454  pjrni  26492  mayete3i  26518  mayete3iOLD  26519  hmopex  26666  cnlnssadj  26871  adjbdln  26874  adjsslnop  26878  shatomistici  27152  hatomistici  27153  xrge0tsmsd  27648  esumpcvgval  27957  hashf2  27963  insiga  28010  sxbrsigalem0  28115  dya2icobrsiga  28120  sxbrsigalem1  28129  sxbrsigalem2  28130  eulerpartlemb  28180  lgamgulm2  28451  lgamcvglem  28455  erdszelem9  28516  erdsze2lem2  28521  kur14lem9  28531  ptpcon  28551  iinllycon  28572  cvmlift3  28646  mppsthm  28812  imagesset  29578  altxpsspw  29602  bpolylem  29785  onsstopbas  29869  onsucconi  29877  onintopsscon  29880  onint1  29889  oninhaus  29890  topjoin  30158  heiborlem3  30284  eldioph3b  30673  diophin  30681  diophun  30682  eldiophss  30683  fz1ssnn  30719  isnumbasabl  31030  isnumbasgrp  31031  dfacbasgrp  31032  mon1psubm  31142  nzin  31199  fzssz  31415  rrpsscn  31510  stoweidlem34  31705  stirlinglem13  31757  fourierdlem20  31798  fourierdlem62  31840  fourierdlem83  31861  fourierdlem101  31879  fourierdlem103  31881  fourierdlem104  31882  fourierdlem111  31889  fouriersw  31903  ringssrng  32407  srhmsubc  32617  srhmsubcOLD  32636  lvecpsslmod  32843  unipwrVD  33365  unipwr  33366  bnj1398  33823  bnj1498  33850  bj-snglss  34276  bj-modssabl  34398  atssbase  34755
  Copyright terms: Public domain W3C validator