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  4329  pwunss  4428  omsson  4760  limom  4761  xpsspw  4887  dmin  4989  dmrnssfld  5045  dmcoss  5052  dminss  5202  imainss  5203  dmxpss  5218  rnxpid  5222  relmptopab  6291  mapfoss  6947  fsetsspwxp  6948  mapsspm  6963  pmsspw  6964  uniixp  7003  snexxph  7267  djuss  7411  pw1on  7586  enq0enq  7799  nqnq0pi  7806  nqnq0  7809  apsscn  8978  aptap  8981  sup3exmid  9290  zssre  9656  zsscn  9657  nnssz  9666  uzssz  9952  divfnzn  10031  zssq  10037  qssre  10040  rpssre  10076  ixxssxr  10313  ixxssixx  10315  iooval2  10328  ioossre  10348  rge0ssre  10390  fzssz  10441  fz1ssnn  10473  fzssuz  10482  fzssp1  10484  uzdisj  10511  fz0ssnn0  10534  nn0disj  10556  fzossfz  10584  fzouzsplit  10599  fzossnn  10613  fzo0ssnn0  10644  infssuzcldc  10679  hashfibc  11299  seq3coll  11310  wrdexb  11332  fclim  12079  bitsss  12731  prmssnn  12909  4sqlem19  13211  restsspw  13656  cntzssv  14154  prdsgrpd  14281  prdsinvgd  14282  ringssrng  14426  subrngintm  14604  subrgintm  14635  cnsubmlem  14999  cnsubglem  15000  znf1o  15070  mplbasss  15178  unitg  15254  cldss2  15298  blssioo  15745  tgioo  15746  limccl  15851  limcresi  15858  dvef  15919  plyssc  15931  reeff1o  15965  griedg0ssusgr  16658  trlsfvalg  16790  clwwlksswrd  16804  clwwlksclwwlkn  16817  bj-omsson  17154