Theorem ssriv 3157

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 3142	. 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 1451	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 2146   C_ wss 3127

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-in 3133  df-ss 3140

This theorem is referenced by:  ssid  3173  ssv  3175  difss  3259  ssun1  3296  inss1  3353  unssdif  3368  inssdif  3369  unssin  3372  inssun  3373  difindiss  3387  undif3ss  3394  0ss  3459  difprsnss  3727  snsspw  3760  pwprss  3801  pwtpss  3802  uniin  3825  iuniin  3892  iundif2ss  3947  iunpwss  3973  pwuni  4187  pwunss  4277  omsson  4606  limom  4607  xpsspw  4732  dmin  4828  dmrnssfld  4883  dmcoss  4889  dminss  5035  imainss  5036  dmxpss  5051  rnxpid  5055  mapsspm  6672  pmsspw  6673  uniixp  6711  snexxph  6939  djuss  7059  pw1on  7215  enq0enq  7405  nqnq0pi  7412  nqnq0  7415  apsscn  8578  sup3exmid  8885  zssre  9231  zsscn  9232  nnssz  9241  uzssz  9518  divfnzn  9592  zssq  9598  qssre  9601  rpssre  9633  ixxssxr  9869  ixxssixx  9871  iooval2  9884  ioossre  9904  rge0ssre  9946  fz1ssnn  10024  fzssuz  10033  fzssp1  10035  uzdisj  10061  fz0ssnn0  10084  nn0disj  10106  fzossfz  10133  fzouzsplit  10147  fzossnn  10157  fzo0ssnn0  10183  seq3coll  10788  fclim  11268  infssuzcldc  11917  prmssnn  12077  restsspw  12618  unitg  13131  cldss2  13175  blssioo  13614  tgioo  13615  limccl  13697  limcresi  13704  dvef  13757  reeff1o  13763  bj-omsson  14272