Step | Hyp | Ref
| Expression |
1 | | dfss2 3901 |
. . 3
⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) |
2 | | idn1 41280 |
. . . . . . 7
⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) ▶ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) ) |
3 | | simpr 488 |
. . . . . . 7
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐵 ⊆ 𝐶) |
4 | 2, 3 | e1a 41333 |
. . . . . 6
⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) ▶ 𝐵 ⊆ 𝐶 ) |
5 | | simpl 486 |
. . . . . . . 8
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐵) |
6 | 2, 5 | e1a 41333 |
. . . . . . 7
⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) ▶ 𝐴 ⊆ 𝐵 ) |
7 | | idn2 41319 |
. . . . . . 7
⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) , 𝑥 ∈ 𝐴 ▶ 𝑥 ∈ 𝐴 ) |
8 | | ssel2 3910 |
. . . . . . 7
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) |
9 | 6, 7, 8 | e12an 41431 |
. . . . . 6
⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) , 𝑥 ∈ 𝐴 ▶ 𝑥 ∈ 𝐵 ) |
10 | | ssel2 3910 |
. . . . . 6
⊢ ((𝐵 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶) |
11 | 4, 9, 10 | e12an 41431 |
. . . . 5
⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) , 𝑥 ∈ 𝐴 ▶ 𝑥 ∈ 𝐶 ) |
12 | 11 | in2 41311 |
. . . 4
⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) ▶ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ) |
13 | 12 | gen11 41322 |
. . 3
⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) ▶ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ) |
14 | | biimpr 223 |
. . 3
⊢ ((𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) → (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → 𝐴 ⊆ 𝐶)) |
15 | 1, 13, 14 | e01 41397 |
. 2
⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) ▶ 𝐴 ⊆ 𝐶 ) |
16 | 15 | in1 41277 |
1
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) |