Theorem ssriv 1508

Description: Inference rule based on subclass definition.

Hypothesis

Ref	Expression
ssriv.1	|- (x e. A -> x e. B)

Assertion

Ref	Expression
ssriv	|- A (_ B

Distinct variable group(s):   x,A   x,B

Proof of Theorem ssriv

Step	Hyp	Ref	Expression
1		dfss2 1497	. 2 |- (A (_ B <-> A.x(x e. A -> x e. B))
2		ssriv.1	. 2 |- (x e. A -> x e. B)
3	1, 2	mpgbir 686	1 |- A (_ B

Syntax hints:   -> wi 2   e. wcel 1092   (_ wss 1487

This theorem is referenced by:  ssv 1520  difss 1596  ssun1 1621  inss1 1657  0ss 1725  snsspw 1857  pwunss 1916  uniin 1935  unipw 1960  pwuni 1961  iuniin 2001  iunpwss 2039  omsson 2377  omssnlim 2386  xpss 2465  dmin 2537  dminss 2648  imainss 2649  tfrlem8 2956  dfom3 3477  tz9.12lem1 3503  rankun 3535  alephsson 3699  cardcf 3706  1pr 3911  reclem2pr 3951  zssre 4569  zsscn 4570  nnssz 4577  zssq 4633  qssre 4636  chsscm 5147  chcmh 5148  omlsi 5250  choc1 5292  shunss 5338  shslej 5339  shsub1 5342  shsub2 5343  shsidm 5358  spanun 5450  spansn 5462  5oalem7 5550  3oalem3 5554  hatomistic 5755

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-in 1491  df-ss 1492

metamath.org