Theorem sstr2 2071

Description: Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17.

Assertion

Ref	Expression
sstr2	|- (A (_ B -> (B (_ C -> A (_ C))

Proof of Theorem sstr2

Step	Hyp	Ref	Expression
1		dfss2 2058	. 2 |- (A (_ B <-> A.x(x e. A -> x e. B))
2		imim1 15	. . . 4 |- ((x e. A -> x e. B) -> ((x e. B -> x e. C) -> (x e. A -> x e. C)))
3	2	19.20ii 995	. . 3 |- (A.x(x e. A -> x e. B) -> (A.x(x e. B -> x e. C) -> A.x(x e. A -> x e. C)))
4		dfss2 2058	. . 3 |- (B (_ C <-> A.x(x e. B -> x e. C))
5		dfss2 2058	. . 3 |- (A (_ C <-> A.x(x e. A -> x e. C))
6	3, 4, 5	3imtr4g 553	. 2 |- (A.x(x e. A -> x e. B) -> (B (_ C -> A (_ C))
7	1, 6	sylbi 199	1 |- (A (_ B -> (B (_ C -> A (_ C))

Syntax hints:   -> wi 3  A.wal 954   e. wcel 958   (_ wss 2047

This theorem is referenced by:  sstr 2072  sstri 2073  sseq1 2082  sseq2 2083  ssun3 2195  ssun4 2196  ssin 2232  ssinss1 2237  ssdisj 2318  sspwb 2755  exss 2769  frss 2921  suceloni 3062  limsssuc 3121  relss 3246  cotr 3436  cnvsym 3437  coexg 3524  funimass2 3573  fss 3635  fco 3636  fssxp 3637  tfrlem1 3911  oaordi 4180  oeworde 4220  sbthlem1 4447  sbthlem2 4448  sbthlem3 4449  sbthlem6 4452  fiint 4559  fiintOLD 4560  abfii4OLD 4564  inf3lem1 4613  trcl 4645  cfle 4913  uzwo3lem2 6217  tgclt 7624  tgsst 7636  tgss2t 7637  clsss 7687  ntrss 7688  neiss 7723  ssnei2 7730  opni3 7866  opnuni 7868  neibl 7877  bcthlem18 8016  chsupval2t 9302  chsupvalt 9303  chsupclt 9308  hsupss 9309  chsupss 9310  spanss 9318  shlej1 9348  shlej1t 9355  chlejb1 9399  stle 10167  dmdbr5 10235  mdsl0 10237  hatomistic 10289  chrelat2 10292  irredlem1 10317  mdsymlem5 10334  mdsymlem6 10335  filintf 10569  rcfpfil 10597  rcfpfilOLD 10598

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053

Copyright terms: Public domain