Theorem ssriv 3252

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 3235	. 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 1506	1 |- A C_ B

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  ssid  3268  ssv  3270  difss  3355  ssun1  3392  inss1  3451  unssdif  3466  inssdif  3467  unssin  3470  inssun  3471  difindiss  3485  undif3ss  3492  0ss  3561  difprsnss  3853  snsspw  3889  pwprss  3931  pwtpss  3932  uniin  3955  iuniin  4022  iundif2ss  4078  iunpwss  4104  pwuni  4331  pwunss  4430  omsson  4762  limom  4763  xpsspw  4889  dmin  4991  dmrnssfld  5047  dmcoss  5054  dminss  5205  imainss  5206  dmxpss  5221  rnxpid  5225  relmptopab  6294  mapfoss  6952  fsetsspwxp  6953  mapsspm  6968  pmsspw  6969  uniixp  7009  snexxph  7274  djuss  7416  pw1on  7591  enq0enq  7804  nqnq0pi  7811  nqnq0  7814  apsscn  8983  aptap  8986  sup3exmid  9295  zssre  9660  zsscn  9661  nnssz  9670  uzssz  9957  divfnzn  10036  zssq  10042  qssre  10045  rpssre  10081  ixxssxr  10318  ixxssixx  10320  iooval2  10333  ioossre  10353  rge0ssre  10395  fzssz  10446  fz1ssnn  10478  fzssuz  10487  fzssp1  10489  uzdisj  10516  fz0ssnn0  10539  nn0disj  10561  fzossfz  10589  fzouzsplit  10604  fzossnn  10618  fzo0ssnn0  10649  infssuzcldc  10684  hashfibc  11304  seq3coll  11315  wrdexb  11337  fclim  12084  bitsss  12736  prmssnn  12914  4sqlem19  13216  restsspw  13661  cntzssv  14159  prdsgrpd  14303  prdsinvgd  14304  ringssrng  14448  subrngintm  14628  subrgintm  14659  cnsubmlem  15023  cnsubglem  15024  znf1o  15094  unitg  15305  cldss2  15349  blssioo  15796  tgioo  15797  limccl  15902  limcresi  15909  dvef  15970  plyssc  15982  reeff1o  16016  griedg0ssusgr  16714  trlsfvalg  16846  clwwlksswrd  16860  clwwlksclwwlkn  16873  bj-omsson  17210