Theorem ssriv 3151

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		dfss2 3136	. 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 1446	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 2141   C_ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  ssid  3167  ssv  3169  difss  3253  ssun1  3290  inss1  3347  unssdif  3362  inssdif  3363  unssin  3366  inssun  3367  difindiss  3381  undif3ss  3388  0ss  3453  difprsnss  3718  snsspw  3751  pwprss  3792  pwtpss  3793  uniin  3816  iuniin  3883  iundif2ss  3938  iunpwss  3964  pwuni  4178  pwunss  4268  omsson  4597  limom  4598  xpsspw  4723  dmin  4819  dmrnssfld  4874  dmcoss  4880  dminss  5025  imainss  5026  dmxpss  5041  rnxpid  5045  mapsspm  6660  pmsspw  6661  uniixp  6699  snexxph  6927  djuss  7047  pw1on  7203  enq0enq  7393  nqnq0pi  7400  nqnq0  7403  apsscn  8566  sup3exmid  8873  zssre  9219  zsscn  9220  nnssz  9229  uzssz  9506  divfnzn  9580  zssq  9586  qssre  9589  rpssre  9621  ixxssxr  9857  ixxssixx  9859  iooval2  9872  ioossre  9892  rge0ssre  9934  fz1ssnn  10012  fzssuz  10021  fzssp1  10023  uzdisj  10049  fz0ssnn0  10072  nn0disj  10094  fzossfz  10121  fzouzsplit  10135  fzossnn  10145  fzo0ssnn0  10171  seq3coll  10777  fclim  11257  infssuzcldc  11906  prmssnn  12066  restsspw  12589  unitg  12856  cldss2  12900  blssioo  13339  tgioo  13340  limccl  13422  limcresi  13429  dvef  13482  reeff1o  13488  bj-omsson  13997