Theorem ssriv 2943

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 2928	. 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 1339	1 |- A C_ B

Syntax hints:   -> wi 4   e. wcel 1390   C_ wss 2911

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 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-in 2918  df-ss 2925

This theorem is referenced by:  ssid  2958  ssv  2959  difss  3064  ssun1  3100  inss1  3151  unssdif  3166  inssdif  3167  unssin  3170  inssun  3171  difindiss  3185  undif3ss  3192  0ss  3249  difprsnss  3493  snsspw  3526  pwprss  3567  pwtpss  3568  uniin  3591  iuniin  3658  iundif2ss  3713  iunpwss  3734  pwuni  3934  pwunss  4011  omsson  4278  limom  4279  xpsspw  4393  dmin  4486  dmrnssfld  4538  dmcoss  4544  dminss  4681  imainss  4682  dmxpss  4696  rnxpid  4698  enq0enq  6414  nqnq0pi  6421  nqnq0  6424  zssre  8028  zsscn  8029  nnssz  8038  uzssz  8268  divfnzn  8332  zssq  8338  qssre  8341  rpssre  8368  ixxssxr  8539  ixxssixx  8541  iooval2  8554  ioossre  8574  rge0ssre  8616  fzssuz  8698  fzssp1  8700  uzdisj  8725  nn0disj  8765  fzossfz  8791  fzouzsplit  8805  fzossnn  8815  fzo0ssnn0  8841  bj-omsson  9422