Theorem ssriv 3232

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 3216	. 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 2202   C_ wss 3201

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  ssid  3248  ssv  3250  difss  3335  ssun1  3372  inss1  3429  unssdif  3444  inssdif  3445  unssin  3448  inssun  3449  difindiss  3463  undif3ss  3470  0ss  3535  difprsnss  3816  snsspw  3852  pwprss  3894  pwtpss  3895  uniin  3918  iuniin  3985  iundif2ss  4041  iunpwss  4067  pwuni  4288  pwunss  4386  omsson  4717  limom  4718  xpsspw  4844  dmin  4945  dmrnssfld  5001  dmcoss  5008  dminss  5158  imainss  5159  dmxpss  5174  rnxpid  5178  relmptopab  6234  mapsspm  6894  pmsspw  6895  uniixp  6933  snexxph  7192  djuss  7312  pw1on  7487  enq0enq  7694  nqnq0pi  7701  nqnq0  7704  apsscn  8869  aptap  8872  sup3exmid  9179  zssre  9530  zsscn  9531  nnssz  9540  uzssz  9820  divfnzn  9899  zssq  9905  qssre  9908  rpssre  9943  ixxssxr  10179  ixxssixx  10181  iooval2  10194  ioossre  10214  rge0ssre  10256  fz1ssnn  10336  fzssuz  10345  fzssp1  10347  uzdisj  10373  fz0ssnn0  10396  nn0disj  10418  fzossfz  10446  fzouzsplit  10461  fzossnn  10475  fzo0ssnn0  10506  infssuzcldc  10541  seq3coll  11152  wrdexb  11174  fclim  11917  bitsss  12569  prmssnn  12747  4sqlem19  13045  restsspw  13395  prdsgrpd  13755  prdsinvgd  13756  ringssrng  14114  subrngintm  14290  subrgintm  14321  cnsubmlem  14657  cnsubglem  14658  znf1o  14730  mplbasss  14780  unitg  14856  cldss2  14900  blssioo  15347  tgioo  15348  limccl  15453  limcresi  15460  dvef  15521  plyssc  15533  reeff1o  15567  griedg0ssusgr  16175  trlsfvalg  16307  clwwlksswrd  16321  clwwlksclwwlkn  16334  bj-omsson  16661