Theorem ssriv 3201

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 3185	. 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 1477	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 2177   C_ wss 3170

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  ssid  3217  ssv  3219  difss  3303  ssun1  3340  inss1  3397  unssdif  3412  inssdif  3413  unssin  3416  inssun  3417  difindiss  3431  undif3ss  3438  0ss  3503  difprsnss  3777  snsspw  3813  pwprss  3855  pwtpss  3856  uniin  3879  iuniin  3946  iundif2ss  4002  iunpwss  4028  pwuni  4247  pwunss  4343  omsson  4674  limom  4675  xpsspw  4800  dmin  4900  dmrnssfld  4955  dmcoss  4962  dminss  5111  imainss  5112  dmxpss  5127  rnxpid  5131  mapsspm  6787  pmsspw  6788  uniixp  6826  snexxph  7073  djuss  7193  pw1on  7367  enq0enq  7574  nqnq0pi  7581  nqnq0  7584  apsscn  8750  aptap  8753  sup3exmid  9060  zssre  9409  zsscn  9410  nnssz  9419  uzssz  9698  divfnzn  9772  zssq  9778  qssre  9781  rpssre  9816  ixxssxr  10052  ixxssixx  10054  iooval2  10067  ioossre  10087  rge0ssre  10129  fz1ssnn  10208  fzssuz  10217  fzssp1  10219  uzdisj  10245  fz0ssnn0  10268  nn0disj  10290  fzossfz  10318  fzouzsplit  10333  fzossnn  10345  fzo0ssnn0  10376  infssuzcldc  10410  seq3coll  11019  wrdexb  11038  fclim  11690  bitsss  12341  prmssnn  12519  4sqlem19  12817  restsspw  13166  prdsgrpd  13526  prdsinvgd  13527  ringssrng  13884  subrngintm  14059  subrgintm  14090  cnsubmlem  14425  cnsubglem  14426  znf1o  14498  mplbasss  14543  unitg  14619  cldss2  14663  blssioo  15110  tgioo  15111  limccl  15216  limcresi  15223  dvef  15284  plyssc  15296  reeff1o  15330  bj-omsson  16067