Theorem ssriv 3101

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		dfss2 3086	. 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 1429	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 1480   C_ wss 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084

This theorem is referenced by:  ssid  3117  ssv  3119  difss  3202  ssun1  3239  inss1  3296  unssdif  3311  inssdif  3312  unssin  3315  inssun  3316  difindiss  3330  undif3ss  3337  0ss  3401  difprsnss  3658  snsspw  3691  pwprss  3732  pwtpss  3733  uniin  3756  iuniin  3823  iundif2ss  3878  iunpwss  3904  pwuni  4116  pwunss  4205  omsson  4526  limom  4527  xpsspw  4651  dmin  4747  dmrnssfld  4802  dmcoss  4808  dminss  4953  imainss  4954  dmxpss  4969  rnxpid  4973  mapsspm  6576  pmsspw  6577  uniixp  6615  snexxph  6838  djuss  6955  enq0enq  7239  nqnq0pi  7246  nqnq0  7249  apsscn  8409  sup3exmid  8715  zssre  9061  zsscn  9062  nnssz  9071  uzssz  9345  divfnzn  9413  zssq  9419  qssre  9422  rpssre  9452  ixxssxr  9683  ixxssixx  9685  iooval2  9698  ioossre  9718  rge0ssre  9760  fz1ssnn  9836  fzssuz  9845  fzssp1  9847  uzdisj  9873  fz0ssnn0  9896  nn0disj  9915  fzossfz  9942  fzouzsplit  9956  fzossnn  9966  fzo0ssnn0  9992  seq3coll  10585  fclim  11063  infssuzcldc  11644  prmssnn  11793  restsspw  12130  unitg  12231  cldss2  12275  blssioo  12714  tgioo  12715  limccl  12797  limcresi  12804  dvef  12856  bj-omsson  13160