Theorem ssriv 3174

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 3159	. 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 1464	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 2160   C_ wss 3144

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157

This theorem is referenced by:  ssid  3190  ssv  3192  difss  3276  ssun1  3313  inss1  3370  unssdif  3385  inssdif  3386  unssin  3389  inssun  3390  difindiss  3404  undif3ss  3411  0ss  3476  difprsnss  3745  snsspw  3779  pwprss  3820  pwtpss  3821  uniin  3844  iuniin  3911  iundif2ss  3967  iunpwss  3993  pwuni  4210  pwunss  4301  omsson  4630  limom  4631  xpsspw  4756  dmin  4853  dmrnssfld  4908  dmcoss  4914  dminss  5061  imainss  5062  dmxpss  5077  rnxpid  5081  mapsspm  6708  pmsspw  6709  uniixp  6747  snexxph  6979  djuss  7099  pw1on  7255  enq0enq  7460  nqnq0pi  7467  nqnq0  7470  apsscn  8634  aptap  8637  sup3exmid  8944  zssre  9290  zsscn  9291  nnssz  9300  uzssz  9577  divfnzn  9651  zssq  9657  qssre  9660  rpssre  9694  ixxssxr  9930  ixxssixx  9932  iooval2  9945  ioossre  9965  rge0ssre  10007  fz1ssnn  10086  fzssuz  10095  fzssp1  10097  uzdisj  10123  fz0ssnn0  10146  nn0disj  10168  fzossfz  10195  fzouzsplit  10209  fzossnn  10219  fzo0ssnn0  10245  seq3coll  10854  fclim  11334  infssuzcldc  11984  prmssnn  12144  4sqlem19  12441  restsspw  12754  ringssrng  13391  subrngintm  13559  subrgintm  13590  cnsubmlem  13881  cnsubglem  13882  unitg  14019  cldss2  14063  blssioo  14502  tgioo  14503  limccl  14585  limcresi  14592  dvef  14645  reeff1o  14651  bj-omsson  15172