Theorem ssriv 3188

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 3172	. 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 1467	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 2167   C_ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  ssid  3204  ssv  3206  difss  3290  ssun1  3327  inss1  3384  unssdif  3399  inssdif  3400  unssin  3403  inssun  3404  difindiss  3418  undif3ss  3425  0ss  3490  difprsnss  3761  snsspw  3795  pwprss  3836  pwtpss  3837  uniin  3860  iuniin  3927  iundif2ss  3983  iunpwss  4009  pwuni  4226  pwunss  4319  omsson  4650  limom  4651  xpsspw  4776  dmin  4875  dmrnssfld  4930  dmcoss  4936  dminss  5085  imainss  5086  dmxpss  5101  rnxpid  5105  mapsspm  6750  pmsspw  6751  uniixp  6789  snexxph  7025  djuss  7145  pw1on  7309  enq0enq  7515  nqnq0pi  7522  nqnq0  7525  apsscn  8691  aptap  8694  sup3exmid  9001  zssre  9350  zsscn  9351  nnssz  9360  uzssz  9638  divfnzn  9712  zssq  9718  qssre  9721  rpssre  9756  ixxssxr  9992  ixxssixx  9994  iooval2  10007  ioossre  10027  rge0ssre  10069  fz1ssnn  10148  fzssuz  10157  fzssp1  10159  uzdisj  10185  fz0ssnn0  10208  nn0disj  10230  fzossfz  10258  fzouzsplit  10272  fzossnn  10282  fzo0ssnn0  10308  infssuzcldc  10342  seq3coll  10951  wrdexb  10964  fclim  11476  bitsss  12127  prmssnn  12305  4sqlem19  12603  restsspw  12951  prdsgrpd  13311  prdsinvgd  13312  ringssrng  13669  subrngintm  13844  subrgintm  13875  cnsubmlem  14210  cnsubglem  14211  znf1o  14283  unitg  14382  cldss2  14426  blssioo  14873  tgioo  14874  limccl  14979  limcresi  14986  dvef  15047  plyssc  15059  reeff1o  15093  bj-omsson  15692