Theorem ssriv 3229

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 3213	. 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 1499	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 2200   C_ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  ssid  3245  ssv  3247  difss  3331  ssun1  3368  inss1  3425  unssdif  3440  inssdif  3441  unssin  3444  inssun  3445  difindiss  3459  undif3ss  3466  0ss  3531  difprsnss  3809  snsspw  3845  pwprss  3887  pwtpss  3888  uniin  3911  iuniin  3978  iundif2ss  4034  iunpwss  4060  pwuni  4280  pwunss  4378  omsson  4709  limom  4710  xpsspw  4836  dmin  4937  dmrnssfld  4993  dmcoss  5000  dminss  5149  imainss  5150  dmxpss  5165  rnxpid  5169  relmptopab  6219  mapsspm  6846  pmsspw  6847  uniixp  6885  snexxph  7140  djuss  7260  pw1on  7434  enq0enq  7641  nqnq0pi  7648  nqnq0  7651  apsscn  8817  aptap  8820  sup3exmid  9127  zssre  9476  zsscn  9477  nnssz  9486  uzssz  9766  divfnzn  9845  zssq  9851  qssre  9854  rpssre  9889  ixxssxr  10125  ixxssixx  10127  iooval2  10140  ioossre  10160  rge0ssre  10202  fz1ssnn  10281  fzssuz  10290  fzssp1  10292  uzdisj  10318  fz0ssnn0  10341  nn0disj  10363  fzossfz  10391  fzouzsplit  10406  fzossnn  10419  fzo0ssnn0  10450  infssuzcldc  10485  seq3coll  11096  wrdexb  11115  fclim  11845  bitsss  12496  prmssnn  12674  4sqlem19  12972  restsspw  13322  prdsgrpd  13682  prdsinvgd  13683  ringssrng  14040  subrngintm  14216  subrgintm  14247  cnsubmlem  14582  cnsubglem  14583  znf1o  14655  mplbasss  14700  unitg  14776  cldss2  14820  blssioo  15267  tgioo  15268  limccl  15373  limcresi  15380  dvef  15441  plyssc  15453  reeff1o  15487  griedg0ssusgr  16090  trlsfvalg  16178  clwwlksswrd  16192  clwwlksclwwlkn  16205  bj-omsson  16493