Theorem ssriv 3228

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 3212	. 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 3197

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 3203  df-ss 3210

This theorem is referenced by:  ssid  3244  ssv  3246  difss  3330  ssun1  3367  inss1  3424  unssdif  3439  inssdif  3440  unssin  3443  inssun  3444  difindiss  3458  undif3ss  3465  0ss  3530  difprsnss  3806  snsspw  3842  pwprss  3884  pwtpss  3885  uniin  3908  iuniin  3975  iundif2ss  4031  iunpwss  4057  pwuni  4276  pwunss  4374  omsson  4705  limom  4706  xpsspw  4831  dmin  4931  dmrnssfld  4987  dmcoss  4994  dminss  5143  imainss  5144  dmxpss  5159  rnxpid  5163  relmptopab  6213  mapsspm  6837  pmsspw  6838  uniixp  6876  snexxph  7128  djuss  7248  pw1on  7422  enq0enq  7629  nqnq0pi  7636  nqnq0  7639  apsscn  8805  aptap  8808  sup3exmid  9115  zssre  9464  zsscn  9465  nnssz  9474  uzssz  9754  divfnzn  9828  zssq  9834  qssre  9837  rpssre  9872  ixxssxr  10108  ixxssixx  10110  iooval2  10123  ioossre  10143  rge0ssre  10185  fz1ssnn  10264  fzssuz  10273  fzssp1  10275  uzdisj  10301  fz0ssnn0  10324  nn0disj  10346  fzossfz  10374  fzouzsplit  10389  fzossnn  10402  fzo0ssnn0  10433  infssuzcldc  10467  seq3coll  11077  wrdexb  11096  fclim  11820  bitsss  12471  prmssnn  12649  4sqlem19  12947  restsspw  13297  prdsgrpd  13657  prdsinvgd  13658  ringssrng  14015  subrngintm  14191  subrgintm  14222  cnsubmlem  14557  cnsubglem  14558  znf1o  14630  mplbasss  14675  unitg  14751  cldss2  14795  blssioo  15242  tgioo  15243  limccl  15348  limcresi  15355  dvef  15416  plyssc  15428  reeff1o  15462  trlsfvalg  16122  clwwlksswrd  16135  bj-omsson  16380