Theorem ssriv 3018

Description: Inference rule 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 3003	. 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 1385	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 1436   C_ wss 2988

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-11 1440  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-in 2994  df-ss 3001

This theorem is referenced by:  ssid  3033  ssv  3035  difss  3115  ssun1  3152  inss1  3209  unssdif  3223  inssdif  3224  unssin  3227  inssun  3228  difindiss  3242  undif3ss  3249  0ss  3309  difprsnss  3557  snsspw  3590  pwprss  3631  pwtpss  3632  uniin  3655  iuniin  3722  iundif2ss  3777  iunpwss  3798  pwuni  3999  pwunss  4082  omsson  4398  limom  4399  xpsspw  4516  dmin  4610  dmrnssfld  4662  dmcoss  4668  dminss  4808  imainss  4809  dmxpss  4823  rnxpid  4827  mapsspm  6384  pmsspw  6385  snexxph  6601  djuun  6696  djuss  6697  enq0enq  6926  nqnq0pi  6933  nqnq0  6936  zssre  8682  zsscn  8683  nnssz  8692  uzssz  8962  divfnzn  9030  zssq  9036  qssre  9039  rpssre  9068  ixxssxr  9242  ixxssixx  9244  iooval2  9257  ioossre  9277  rge0ssre  9319  fzssuz  9402  fzssp1  9404  uzdisj  9429  nn0disj  9469  fzossfz  9496  fzouzsplit  9510  fzossnn  9520  fzo0ssnn0  9546  iseqcoll  10135  fclim  10567  infssuzcldc  10813  prmssnn  10960  bj-omsson  11286