Theorem ssriv 3607

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

Step	Hyp	Ref	Expression
1		dfss2 3591	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2		ssriv.1	. 2 |- ( x e. A -> x e. B )
3	1, 2	mpgbir 1726	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 1990   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  ssid  3624  ssv  3625  difss  3737  ssun1  3776  inss1  3833  0ss  3972  difprsnss  4329  snsspw  4375  uniin  4457  pwuni  4474  iuniin  4531  iunpwss  4618  pwunss  5019  relopabi  5245  dmin  5332  dmrnssfld  5384  dmcoss  5385  dminss  5547  imainss  5548  fviss  6256  mapsspm  7891  pmsspw  7892  uniixp  7931  pwfilem  8260  dffi3  8337  dfom3  8544  onwf  8693  tcrank  8747  cardprclem  8805  alephsson  8923  ackbij1  9060  cardcf  9074  cfeq0  9078  dfacfin7  9221  hsmexlem6  9253  canthnum  9471  inaprc  9658  nqerf  9752  addnqf  9770  mulnqf  9771  dmrecnq  9790  reclem2pr  9870  wuncn  9991  zssre  11384  zsscn  11385  nnssz  11397  elq  11790  zssq  11795  qssre  11798  rpssre  11843  ixxssixx  12189  iooval2  12208  ioossre  12235  rge0ssre  12280  fzssz  12343  fz1ssnn  12372  fzssuz  12382  fzssp1  12384  uzdisj  12413  fz0ssnn0  12435  nn0disj  12455  fzossfz  12488  fzouzsplit  12503  fzossnn  12516  fzo0ssnn0  12548  fzo0ssnn0OLD  12549  uzrdgfni  12757  seqcoll  13248  wrdexg  13315  wrdexb  13316  fclim  14284  isercolllem3  14397  isercoll  14398  climcnds  14583  divcnv  14585  harmonic  14591  fprodge0  14724  bitsss  15148  prmssnn  15390  maxprmfct  15421  prminf  15619  prmreclem3  15622  1arithlem1  15627  1arith  15631  4sqlem19  15667  vdwlem12  15696  restsspw  16092  xpsc0  16220  xpsc1  16221  mremre  16264  mreacs  16319  isfunc  16524  homarel  16686  ledm  17224  lern  17225  sgrpssmgm  17420  mndsssgrp  17421  prdsgrpd  17525  prdsinvgd  17526  symgtrf  17889  odf1o2  17988  sylow3lem3  18044  sylow3lem6  18047  oppglsm  18057  efgsfo  18152  0frgp  18192  prdscmnd  18264  prdsabld  18265  dprdssv  18415  dprdres  18427  ablfac1b  18469  prdsringd  18612  prdscrngd  18613  unitss  18660  subrgint  18802  lssintcl  18964  prdslmodd  18969  xrge0subm  19787  cnsubmlem  19794  cnsubglem  19795  cnsubdrglem  19797  cnmsubglem  19809  zringunit  19836  zringlpir  19837  znf1o  19900  zntoslem  19905  ocvss  20014  dsmmsubg  20087  dsmmlss  20088  lbslinds  20172  unitg  20771  cldss2  20834  indiscld  20895  toponmre  20897  iscldtop  20899  1stcfb  21248  llyssnlly  21281  llyidm  21291  nllyidm  21292  toplly  21293  hauslly  21295  lly1stc  21299  dissnref  21331  1stckgenlem  21356  txindis  21437  pthaus  21441  ptcmpfi  21616  ufinffr  21733  cnflf2  21807  flimfcls  21830  alexsubALTlem3  21853  ptcmplem1  21856  ptcmpg  21861  prdstmdd  21927  prdstgpd  21928  ust0  22023  prdsms  22336  qdensere  22573  blssioo  22598  tgioo  22599  xrtgioo  22609  xrsmopn  22615  zdis  22619  reperflem  22621  xrge0gsumle  22636  xrge0tsms  22637  icopnfhmeo  22742  bndth  22757  ovoliunlem1  23270  ovoliun2  23274  ovolicc2lem4  23288  voliunlem2  23319  voliunlem3  23320  uniioovol  23347  uniioombllem4  23354  vitali  23382  ismbf3d  23421  itg2seq  23509  limccl  23639  limcresi  23649  dvef  23743  aasscn  24073  qssaa  24079  aannenlem2  24084  aannenlem3  24085  ulmcn  24153  mtestbdd  24159  iblulm  24161  reeff1o  24201  reefgim  24204  efifo  24293  dfrelog  24312  relogf1o  24313  logdmss  24388  logcn  24393  dvloglem  24394  logf1o2  24396  dvlog  24397  dvlog2lem  24398  dvlog2  24399  logtayl  24406  cxpcn  24486  cxpcn2  24487  cxpcn3  24489  resqrtcn  24490  efrlim  24696  dfef2  24697  cxp2lim  24703  wilthlem2  24795  wilthlem3  24796  basellem3  24809  basellem4  24810  prmdvdsfi  24833  vmaval  24839  mumul  24907  sqff1o  24908  musum  24917  fsumvma2  24939  dchrmhm  24966  chtppilim  25164  chto1lb  25167  chpchtlim  25168  chpo1ub  25169  dchrisumlema  25177  dchrmusum2  25183  dchrvmasum2lem  25185  dirith2  25217  mudivsum  25219  mulogsum  25221  mulog2sumlem2  25224  selberg2lem  25239  selberg3lem2  25247  pntrsumo1  25254  pnt2  25302  pnt  25303  axcontlem2  25845  usgrexmplef  26151  griedg0ssusgr  26157  uvtxassvtx  26290  rgrusgrprc  26485  clwlkswks  26672  wwlkssswrd  26747  wwlkssswwlksn  26751  wspthsswwlkn  26814  wspthsswwlknon  26817  clwwlkssclwwlksn  26892  phrel  27670  bnrel  27723  hlrel  27746  shex  28069  chsssh  28082  hhssnv  28121  choc1  28186  shunssi  28227  shsleji  28229  shsub1i  28231  shsub2i  28232  shsidmi  28243  omlsii  28262  spanuni  28403  spansni  28416  5oalem7  28519  3oalem3  28523  pjrni  28561  mayete3i  28587  hmopex  28734  cnlnssadj  28939  adjbdln  28942  adjsslnop  28946  shatomistici  29220  hatomistici  29221  xrge0tsmsd  29785  esumpcvgval  30140  hashf2  30146  insiga  30200  sigapisys  30218  sigaldsys  30222  sigapildsys  30225  sxbrsigalem0  30333  dya2icobrsiga  30338  sxbrsigalem1  30347  sxbrsigalem2  30348  eulerpartlemb  30430  chtvalz  30707  logdivsqrle  30728  bnj1398  31102  bnj1498  31129  erdszelem9  31181  erdsze2lem2  31186  kur14lem9  31196  ptpconn  31215  iinllyconn  31236  cvmlift3  31310  mppsthm  31476  imagesset  32060  altxpsspw  32084  topjoin  32360  onsstopbas  32428  onsucconni  32436  onintopssconn  32439  onint1  32448  oninhaus  32449  bj-snglss  32958  bj-modssabl  33142  icoreunrn  33207  poimirlem8  33417  poimirlem18  33427  poimirlem21  33430  poimirlem22  33431  poimirlem31  33440  poimirlem32  33441  heiborlem3  33612  atssbase  34577  eldioph3b  37328  diophin  37336  diophun  37337  eldiophss  37338  isnumbasabl  37676  isnumbasgrp  37677  dfacbasgrp  37678  mon1psubm  37784  inintabss  37884  intimass  37946  nzin  38517  unipwrVD  39067  unipwr  39068  supxrre3  39541  fsumiunss  39807  rrpsscn  39820  dvnmul  40158  dvnprodlem2  40162  stoweidlem34  40251  stirlinglem13  40303  fourierdlem20  40344  fourierdlem62  40385  fourierdlem83  40406  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fouriersw  40448  qndenserrnbllem  40514  sge0iunmptlemre  40632  nn0ssge0  40641  sge0isum  40644  sge0seq  40663  sge0reuz  40664  caragendifcl  40728  carageniuncllem2  40736  hoicvrrex  40770  smfaddlem1  40971  smfaddlem2  40972  mbfpsssmf  40991  ringssrng  41880  srhmsubc  42076  srhmsubcALTV  42094  lvecpsslmod  42296  aacllem  42547  amgmwlem  42548  amgmlemALT  42549