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  7410  pw1on  7585  enq0enq  7798  nqnq0pi  7805  nqnq0  7808  apsscn  8977  aptap  8980  sup3exmid  9289  zssre  9655  zsscn  9656  nnssz  9665  uzssz  9951  divfnzn  10030  zssq  10036  qssre  10039  rpssre  10075  ixxssxr  10312  ixxssixx  10314  iooval2  10327  ioossre  10347  rge0ssre  10389  fzssz  10440  fz1ssnn  10472  fzssuz  10481  fzssp1  10483  uzdisj  10510  fz0ssnn0  10533  nn0disj  10555  fzossfz  10583  fzouzsplit  10598  fzossnn  10612  fzo0ssnn0  10643  infssuzcldc  10678  hashfibc  11297  seq3coll  11308  wrdexb  11330  fclim  12076  bitsss  12728  prmssnn  12906  4sqlem19  13208  restsspw  13652  prdsgrpd  14246  prdsinvgd  14247  ringssrng  14391  subrngintm  14569  subrgintm  14600  cnsubmlem  14964  cnsubglem  14965  znf1o  15035  mplbasss  15136  unitg  15212  cldss2  15256  blssioo  15703  tgioo  15704  limccl  15809  limcresi  15816  dvef  15877  plyssc  15889  reeff1o  15923  griedg0ssusgr  16590  trlsfvalg  16722  clwwlksswrd  16736  clwwlksclwwlkn  16749  bj-omsson  17086