Theorem ssriv 3187

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		dfss2 3172	. 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 1467	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 2167   C_ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  ssid  3203  ssv  3205  difss  3289  ssun1  3326  inss1  3383  unssdif  3398  inssdif  3399  unssin  3402  inssun  3403  difindiss  3417  undif3ss  3424  0ss  3489  difprsnss  3760  snsspw  3794  pwprss  3835  pwtpss  3836  uniin  3859  iuniin  3926  iundif2ss  3982  iunpwss  4008  pwuni  4225  pwunss  4318  omsson  4649  limom  4650  xpsspw  4775  dmin  4874  dmrnssfld  4929  dmcoss  4935  dminss  5084  imainss  5085  dmxpss  5100  rnxpid  5104  mapsspm  6741  pmsspw  6742  uniixp  6780  snexxph  7016  djuss  7136  pw1on  7293  enq0enq  7498  nqnq0pi  7505  nqnq0  7508  apsscn  8674  aptap  8677  sup3exmid  8984  zssre  9333  zsscn  9334  nnssz  9343  uzssz  9621  divfnzn  9695  zssq  9701  qssre  9704  rpssre  9739  ixxssxr  9975  ixxssixx  9977  iooval2  9990  ioossre  10010  rge0ssre  10052  fz1ssnn  10131  fzssuz  10140  fzssp1  10142  uzdisj  10168  fz0ssnn0  10191  nn0disj  10213  fzossfz  10241  fzouzsplit  10255  fzossnn  10265  fzo0ssnn0  10291  infssuzcldc  10325  seq3coll  10934  wrdexb  10947  fclim  11459  bitsss  12110  prmssnn  12280  4sqlem19  12578  restsspw  12920  ringssrng  13593  subrngintm  13768  subrgintm  13799  cnsubmlem  14134  cnsubglem  14135  znf1o  14207  unitg  14298  cldss2  14342  blssioo  14789  tgioo  14790  limccl  14895  limcresi  14902  dvef  14963  plyssc  14975  reeff1o  15009  bj-omsson  15608