Theorem ssriv 3197

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 3181	. 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 1476	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 2176   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  ssid  3213  ssv  3215  difss  3299  ssun1  3336  inss1  3393  unssdif  3408  inssdif  3409  unssin  3412  inssun  3413  difindiss  3427  undif3ss  3434  0ss  3499  difprsnss  3771  snsspw  3805  pwprss  3846  pwtpss  3847  uniin  3870  iuniin  3937  iundif2ss  3993  iunpwss  4019  pwuni  4236  pwunss  4330  omsson  4661  limom  4662  xpsspw  4787  dmin  4886  dmrnssfld  4941  dmcoss  4948  dminss  5097  imainss  5098  dmxpss  5113  rnxpid  5117  mapsspm  6769  pmsspw  6770  uniixp  6808  snexxph  7052  djuss  7172  pw1on  7338  enq0enq  7544  nqnq0pi  7551  nqnq0  7554  apsscn  8720  aptap  8723  sup3exmid  9030  zssre  9379  zsscn  9380  nnssz  9389  uzssz  9668  divfnzn  9742  zssq  9748  qssre  9751  rpssre  9786  ixxssxr  10022  ixxssixx  10024  iooval2  10037  ioossre  10057  rge0ssre  10099  fz1ssnn  10178  fzssuz  10187  fzssp1  10189  uzdisj  10215  fz0ssnn0  10238  nn0disj  10260  fzossfz  10288  fzouzsplit  10303  fzossnn  10313  fzo0ssnn0  10344  infssuzcldc  10378  seq3coll  10987  wrdexb  11006  fclim  11605  bitsss  12256  prmssnn  12434  4sqlem19  12732  restsspw  13081  prdsgrpd  13441  prdsinvgd  13442  ringssrng  13799  subrngintm  13974  subrgintm  14005  cnsubmlem  14340  cnsubglem  14341  znf1o  14413  mplbasss  14458  unitg  14534  cldss2  14578  blssioo  15025  tgioo  15026  limccl  15131  limcresi  15138  dvef  15199  plyssc  15211  reeff1o  15245  bj-omsson  15898