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  6413  nqnq0pi  6420  nqnq0  6423  zssre  8008  zsscn  8009  nnssz  8018  uzssz  8248  divfnzn  8312  zssq  8318  qssre  8321  rpssre  8348  ixxssxr  8519  ixxssixx  8521  iooval2  8534  ioossre  8554  rge0ssre  8596  fzssuz  8678  fzssp1  8680  uzdisj  8705  nn0disj  8745  fzossfz  8771  fzouzsplit  8785  fzossnn  8795  fzo0ssnn0  8821