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  6951  fsetsspwxp  6952  mapsspm  6967  pmsspw  6968  uniixp  7007  snexxph  7272  djuss  7416  pw1on  7591  enq0enq  7804  nqnq0pi  7811  nqnq0  7814  apsscn  8983  aptap  8986  sup3exmid  9295  zssre  9662  zsscn  9663  nnssz  9672  uzssz  9958  divfnzn  10037  zssq  10043  qssre  10046  rpssre  10082  ixxssxr  10319  ixxssixx  10321  iooval2  10334  ioossre  10354  rge0ssre  10396  fzssz  10447  fz1ssnn  10479  fzssuz  10488  fzssp1  10490  uzdisj  10517  fz0ssnn0  10540  nn0disj  10562  fzossfz  10590  fzouzsplit  10605  fzossnn  10619  fzo0ssnn0  10650  infssuzcldc  10685  hashfibc  11305  seq3coll  11316  wrdexb  11338  fclim  12085  bitsss  12737  prmssnn  12915  4sqlem19  13217  restsspw  13662  cntzssv  14160  prdsgrpd  14304  prdsinvgd  14305  ringssrng  14449  subrngintm  14629  subrgintm  14660  cnsubmlem  15024  cnsubglem  15025  znf1o  15095  mplbasss  15212  unitg  15288  cldss2  15332  blssioo  15779  tgioo  15780  limccl  15885  limcresi  15892  dvef  15953  plyssc  15965  reeff1o  15999  griedg0ssusgr  16697  trlsfvalg  16829  clwwlksswrd  16843  clwwlksclwwlkn  16856  bj-omsson  17193