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  3805  snsspw  3841  pwprss  3883  pwtpss  3884  uniin  3907  iuniin  3974  iundif2ss  4030  iunpwss  4056  pwuni  4275  pwunss  4373  omsson  4704  limom  4705  xpsspw  4830  dmin  4930  dmrnssfld  4986  dmcoss  4993  dminss  5142  imainss  5143  dmxpss  5158  rnxpid  5162  mapsspm  6827  pmsspw  6828  uniixp  6866  snexxph  7113  djuss  7233  pw1on  7407  enq0enq  7614  nqnq0pi  7621  nqnq0  7624  apsscn  8790  aptap  8793  sup3exmid  9100  zssre  9449  zsscn  9450  nnssz  9459  uzssz  9738  divfnzn  9812  zssq  9818  qssre  9821  rpssre  9856  ixxssxr  10092  ixxssixx  10094  iooval2  10107  ioossre  10127  rge0ssre  10169  fz1ssnn  10248  fzssuz  10257  fzssp1  10259  uzdisj  10285  fz0ssnn0  10308  nn0disj  10330  fzossfz  10358  fzouzsplit  10373  fzossnn  10385  fzo0ssnn0  10416  infssuzcldc  10450  seq3coll  11059  wrdexb  11078  fclim  11800  bitsss  12451  prmssnn  12629  4sqlem19  12927  restsspw  13277  prdsgrpd  13637  prdsinvgd  13638  ringssrng  13995  subrngintm  14170  subrgintm  14201  cnsubmlem  14536  cnsubglem  14537  znf1o  14609  mplbasss  14654  unitg  14730  cldss2  14774  blssioo  15221  tgioo  15222  limccl  15327  limcresi  15334  dvef  15395  plyssc  15407  reeff1o  15441  bj-omsson  16283