Theorem ssriv 3246

Description: Inference based on subclass definition. (Contributed by NM, 5-Aug-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		ssalel 3229	. 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 1502	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 2205   C_ wss 3214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  ssid  3262  ssv  3264  difss  3349  ssun1  3386  inss1  3445  unssdif  3460  inssdif  3461  unssin  3464  inssun  3465  difindiss  3479  undif3ss  3486  0ss  3551  difprsnss  3837  snsspw  3873  pwprss  3915  pwtpss  3916  uniin  3939  iuniin  4006  iundif2ss  4062  iunpwss  4088  pwuni  4310  pwunss  4409  omsson  4740  limom  4741  xpsspw  4867  dmin  4969  dmrnssfld  5025  dmcoss  5032  dminss  5182  imainss  5183  dmxpss  5198  rnxpid  5202  relmptopab  6264  mapsspm  6929  pmsspw  6930  uniixp  6969  snexxph  7233  djuss  7374  pw1on  7549  enq0enq  7762  nqnq0pi  7769  nqnq0  7772  apsscn  8938  aptap  8941  sup3exmid  9248  zssre  9601  zsscn  9602  nnssz  9611  uzssz  9892  divfnzn  9971  zssq  9977  qssre  9980  rpssre  10015  ixxssxr  10252  ixxssixx  10254  iooval2  10267  ioossre  10287  rge0ssre  10329  fzssz  10380  fz1ssnn  10411  fzssuz  10420  fzssp1  10422  uzdisj  10449  fz0ssnn0  10472  nn0disj  10494  fzossfz  10522  fzouzsplit  10537  fzossnn  10551  fzo0ssnn0  10582  infssuzcldc  10617  hashfibc  11232  seq3coll  11239  wrdexb  11261  fclim  12004  bitsss  12656  prmssnn  12834  4sqlem19  13132  restsspw  13546  prdsgrpd  14139  prdsinvgd  14140  ringssrng  14280  subrngintm  14458  subrgintm  14489  cnsubmlem  14852  cnsubglem  14853  znf1o  14925  mplbasss  14977  unitg  15053  cldss2  15097  blssioo  15544  tgioo  15545  limccl  15650  limcresi  15657  dvef  15718  plyssc  15730  reeff1o  15764  griedg0ssusgr  16372  trlsfvalg  16504  clwwlksswrd  16518  clwwlksclwwlkn  16531  bj-omsson  16858