Theorem ssriv 3196

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 3180	. 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 1475	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 2175   C_ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  ssid  3212  ssv  3214  difss  3298  ssun1  3335  inss1  3392  unssdif  3407  inssdif  3408  unssin  3411  inssun  3412  difindiss  3426  undif3ss  3433  0ss  3498  difprsnss  3770  snsspw  3804  pwprss  3845  pwtpss  3846  uniin  3869  iuniin  3936  iundif2ss  3992  iunpwss  4018  pwuni  4235  pwunss  4329  omsson  4660  limom  4661  xpsspw  4786  dmin  4885  dmrnssfld  4940  dmcoss  4947  dminss  5096  imainss  5097  dmxpss  5112  rnxpid  5116  mapsspm  6768  pmsspw  6769  uniixp  6807  snexxph  7051  djuss  7171  pw1on  7337  enq0enq  7543  nqnq0pi  7550  nqnq0  7553  apsscn  8719  aptap  8722  sup3exmid  9029  zssre  9378  zsscn  9379  nnssz  9388  uzssz  9667  divfnzn  9741  zssq  9747  qssre  9750  rpssre  9785  ixxssxr  10021  ixxssixx  10023  iooval2  10036  ioossre  10056  rge0ssre  10098  fz1ssnn  10177  fzssuz  10186  fzssp1  10188  uzdisj  10214  fz0ssnn0  10237  nn0disj  10259  fzossfz  10287  fzouzsplit  10301  fzossnn  10311  fzo0ssnn0  10342  infssuzcldc  10376  seq3coll  10985  wrdexb  11004  fclim  11576  bitsss  12227  prmssnn  12405  4sqlem19  12703  restsspw  13052  prdsgrpd  13412  prdsinvgd  13413  ringssrng  13770  subrngintm  13945  subrgintm  13976  cnsubmlem  14311  cnsubglem  14312  znf1o  14384  mplbasss  14429  unitg  14505  cldss2  14549  blssioo  14996  tgioo  14997  limccl  15102  limcresi  15109  dvef  15170  plyssc  15182  reeff1o  15216  bj-omsson  15860