Theorem ssriv 3067

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 3052	. 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 1412	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 1463   C_ wss 3037

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3043  df-ss 3050

This theorem is referenced by:  ssid  3083  ssv  3085  difss  3168  ssun1  3205  inss1  3262  unssdif  3277  inssdif  3278  unssin  3281  inssun  3282  difindiss  3296  undif3ss  3303  0ss  3367  difprsnss  3624  snsspw  3657  pwprss  3698  pwtpss  3699  uniin  3722  iuniin  3789  iundif2ss  3844  iunpwss  3870  pwuni  4076  pwunss  4165  omsson  4486  limom  4487  xpsspw  4611  dmin  4707  dmrnssfld  4760  dmcoss  4766  dminss  4911  imainss  4912  dmxpss  4927  rnxpid  4931  mapsspm  6530  pmsspw  6531  uniixp  6569  snexxph  6790  djuss  6907  enq0enq  7187  nqnq0pi  7194  nqnq0  7197  sup3exmid  8625  zssre  8965  zsscn  8966  nnssz  8975  uzssz  9247  divfnzn  9315  zssq  9321  qssre  9324  rpssre  9353  ixxssxr  9576  ixxssixx  9578  iooval2  9591  ioossre  9611  rge0ssre  9653  fz1ssnn  9729  fzssuz  9738  fzssp1  9740  uzdisj  9766  fz0ssnn0  9789  nn0disj  9808  fzossfz  9835  fzouzsplit  9849  fzossnn  9859  fzo0ssnn0  9885  seq3coll  10478  fclim  10955  infssuzcldc  11492  prmssnn  11639  restsspw  11973  unitg  12074  cldss2  12118  blssioo  12531  tgioo  12532  limccl  12584  limcresi  12591  bj-omsson  12852