Theorem ssriv 3252

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 3235	. 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 1506	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 2209   C_ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  ssid  3268  ssv  3270  difss  3355  ssun1  3392  inss1  3451  unssdif  3466  inssdif  3467  unssin  3470  inssun  3471  difindiss  3485  undif3ss  3492  0ss  3561  difprsnss  3848  snsspw  3884  pwprss  3926  pwtpss  3927  uniin  3950  iuniin  4017  iundif2ss  4073  iunpwss  4099  pwuni  4324  pwunss  4423  omsson  4755  limom  4756  xpsspw  4882  dmin  4984  dmrnssfld  5040  dmcoss  5047  dminss  5197  imainss  5198  dmxpss  5213  rnxpid  5217  relmptopab  6281  mapfoss  6937  fsetsspwxp  6938  mapsspm  6953  pmsspw  6954  uniixp  6993  snexxph  7257  djuss  7400  pw1on  7575  enq0enq  7788  nqnq0pi  7795  nqnq0  7798  apsscn  8965  aptap  8968  sup3exmid  9277  zssre  9630  zsscn  9631  nnssz  9640  uzssz  9921  divfnzn  10000  zssq  10006  qssre  10009  rpssre  10044  ixxssxr  10281  ixxssixx  10283  iooval2  10296  ioossre  10316  rge0ssre  10358  fzssz  10409  fz1ssnn  10440  fzssuz  10449  fzssp1  10451  uzdisj  10478  fz0ssnn0  10501  nn0disj  10523  fzossfz  10551  fzouzsplit  10566  fzossnn  10580  fzo0ssnn0  10611  infssuzcldc  10646  hashfibc  11261  seq3coll  11272  wrdexb  11294  fclim  12038  bitsss  12690  prmssnn  12868  4sqlem19  13166  restsspw  13580  prdsgrpd  14174  prdsinvgd  14175  ringssrng  14315  subrngintm  14493  subrgintm  14524  cnsubmlem  14887  cnsubglem  14888  znf1o  14958  mplbasss  15010  unitg  15086  cldss2  15130  blssioo  15577  tgioo  15578  limccl  15683  limcresi  15690  dvef  15751  plyssc  15763  reeff1o  15797  griedg0ssusgr  16406  trlsfvalg  16538  clwwlksswrd  16552  clwwlksclwwlkn  16565  bj-omsson  16902