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  8975  aptap  8978  sup3exmid  9287  zssre  9651  zsscn  9652  nnssz  9661  uzssz  9942  divfnzn  10021  zssq  10027  qssre  10030  rpssre  10065  ixxssxr  10302  ixxssixx  10304  iooval2  10317  ioossre  10337  rge0ssre  10379  fzssz  10430  fz1ssnn  10462  fzssuz  10471  fzssp1  10473  uzdisj  10500  fz0ssnn0  10523  nn0disj  10545  fzossfz  10573  fzouzsplit  10588  fzossnn  10602  fzo0ssnn0  10633  infssuzcldc  10668  hashfibc  11283  seq3coll  11294  wrdexb  11316  fclim  12060  bitsss  12712  prmssnn  12890  4sqlem19  13188  restsspw  13603  prdsgrpd  14197  prdsinvgd  14198  ringssrng  14342  subrngintm  14520  subrgintm  14551  cnsubmlem  14915  cnsubglem  14916  znf1o  14986  mplbasss  15087  unitg  15163  cldss2  15207  blssioo  15654  tgioo  15655  limccl  15760  limcresi  15767  dvef  15828  plyssc  15840  reeff1o  15874  griedg0ssusgr  16492  trlsfvalg  16624  clwwlksswrd  16638  clwwlksclwwlkn  16651  bj-omsson  16988