Theorem sstr2 3190

Description: Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)

Assertion

Ref	Expression
sstr2	⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))

Proof of Theorem sstr2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3177	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	imim1d 75	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
3	2	alimdv 1893	. 2 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
4		dfss2 3172	. 2 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
5		dfss2 3172	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6	3, 4, 5	3imtr4g 205	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))

Syntax hints:   → wi 4  ∀wal 1362   ∈ wcel 2167   ⊆ wss 3157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  sstr  3191  sstri  3192  sseq1  3206  sseq2  3207  ssun3  3328  ssun4  3329  ssinss1  3392  ssdisj  3507  triun  4144  trintssm  4147  sspwb  4249  exss  4260  relss  4750  funss  5277  funimass2  5336  fss  5419  fiintim  6992  sbthlem2  7024  sbthlemi3  7025  sbthlemi6  7028  lsslss  13937  lspss  13955  tgss  14299  tgcl  14300  tgss3  14314  clsss  14354  neiss  14386  ssnei2  14393  cnpnei  14455  cnptopco  14458  cnptoprest  14475  txcnp  14507  neibl  14727  metcnp3  14747  bj-nntrans  15597