Theorem ssriv 3161

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 3146	. 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 1453	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 2148   C_ wss 3131

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  ssid  3177  ssv  3179  difss  3263  ssun1  3300  inss1  3357  unssdif  3372  inssdif  3373  unssin  3376  inssun  3377  difindiss  3391  undif3ss  3398  0ss  3463  difprsnss  3732  snsspw  3766  pwprss  3807  pwtpss  3808  uniin  3831  iuniin  3898  iundif2ss  3954  iunpwss  3980  pwuni  4194  pwunss  4285  omsson  4614  limom  4615  xpsspw  4740  dmin  4837  dmrnssfld  4892  dmcoss  4898  dminss  5045  imainss  5046  dmxpss  5061  rnxpid  5065  mapsspm  6684  pmsspw  6685  uniixp  6723  snexxph  6951  djuss  7071  pw1on  7227  enq0enq  7432  nqnq0pi  7439  nqnq0  7442  apsscn  8606  aptap  8609  sup3exmid  8916  zssre  9262  zsscn  9263  nnssz  9272  uzssz  9549  divfnzn  9623  zssq  9629  qssre  9632  rpssre  9666  ixxssxr  9902  ixxssixx  9904  iooval2  9917  ioossre  9937  rge0ssre  9979  fz1ssnn  10058  fzssuz  10067  fzssp1  10069  uzdisj  10095  fz0ssnn0  10118  nn0disj  10140  fzossfz  10167  fzouzsplit  10181  fzossnn  10191  fzo0ssnn0  10217  seq3coll  10824  fclim  11304  infssuzcldc  11954  prmssnn  12114  restsspw  12703  subrgintm  13369  cnsubmlem  13511  cnsubglem  13512  unitg  13601  cldss2  13645  blssioo  14084  tgioo  14085  limccl  14167  limcresi  14174  dvef  14227  reeff1o  14233  bj-omsson  14753