Theorem ssriv 3242

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 3226	. 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 1502	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 2203   C_ wss 3211

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  ssid  3258  ssv  3260  difss  3345  ssun1  3382  inss1  3441  unssdif  3456  inssdif  3457  unssin  3460  inssun  3461  difindiss  3475  undif3ss  3482  0ss  3547  difprsnss  3832  snsspw  3868  pwprss  3910  pwtpss  3911  uniin  3934  iuniin  4001  iundif2ss  4057  iunpwss  4083  pwuni  4305  pwunss  4404  omsson  4735  limom  4736  xpsspw  4862  dmin  4964  dmrnssfld  5020  dmcoss  5027  dminss  5177  imainss  5178  dmxpss  5193  rnxpid  5197  relmptopab  6256  mapsspm  6916  pmsspw  6917  uniixp  6956  snexxph  7220  djuss  7361  pw1on  7536  enq0enq  7746  nqnq0pi  7753  nqnq0  7756  apsscn  8921  aptap  8924  sup3exmid  9231  zssre  9584  zsscn  9585  nnssz  9594  uzssz  9874  divfnzn  9953  zssq  9959  qssre  9962  rpssre  9997  ixxssxr  10233  ixxssixx  10235  iooval2  10248  ioossre  10268  rge0ssre  10310  fz1ssnn  10390  fzssuz  10399  fzssp1  10401  uzdisj  10427  fz0ssnn0  10450  nn0disj  10472  fzossfz  10500  fzouzsplit  10515  fzossnn  10529  fzo0ssnn0  10560  infssuzcldc  10595  hashfibc  11207  seq3coll  11214  wrdexb  11236  fclim  11979  bitsss  12631  prmssnn  12809  4sqlem19  13107  restsspw  13462  prdsgrpd  13822  prdsinvgd  13823  ringssrng  14181  subrngintm  14357  subrgintm  14388  cnsubmlem  14726  cnsubglem  14727  znf1o  14799  mplbasss  14851  unitg  14927  cldss2  14971  blssioo  15418  tgioo  15419  limccl  15524  limcresi  15531  dvef  15592  plyssc  15604  reeff1o  15638  griedg0ssusgr  16246  trlsfvalg  16378  clwwlksswrd  16392  clwwlksclwwlkn  16405  bj-omsson  16732