Theorem ssriv 2949

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 2934	. 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 1342	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 1393   C_ wss 2917

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-in 2924  df-ss 2931

This theorem is referenced by:  ssid  2964  ssv  2965  difss  3070  ssun1  3106  inss1  3157  unssdif  3172  inssdif  3173  unssin  3176  inssun  3177  difindiss  3191  undif3ss  3198  0ss  3255  difprsnss  3502  snsspw  3535  pwprss  3576  pwtpss  3577  uniin  3600  iuniin  3667  iundif2ss  3722  iunpwss  3743  pwuni  3943  pwunss  4020  omsson  4335  limom  4336  xpsspw  4450  dmin  4543  dmrnssfld  4595  dmcoss  4601  dminss  4738  imainss  4739  dmxpss  4753  rnxpid  4755  enq0enq  6529  nqnq0pi  6536  nqnq0  6539  zssre  8252  zsscn  8253  nnssz  8262  uzssz  8492  divfnzn  8556  zssq  8562  qssre  8565  rpssre  8593  ixxssxr  8769  ixxssixx  8771  iooval2  8784  ioossre  8804  rge0ssre  8846  fzssuz  8928  fzssp1  8930  uzdisj  8955  nn0disj  8995  fzossfz  9021  fzouzsplit  9035  fzossnn  9045  fzo0ssnn0  9071  fclim  9815  bj-omsson  10087