| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-ss 3968 | . . 3
⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) | 
| 2 |  | idn1 44594 | . . . . . . 7
⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶)   ▶   (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶)   ) | 
| 3 |  | simpr 484 | . . . . . . 7
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐵 ⊆ 𝐶) | 
| 4 | 2, 3 | e1a 44647 | . . . . . 6
⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶)   ▶   𝐵 ⊆ 𝐶   ) | 
| 5 |  | simpl 482 | . . . . . . . 8
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐵) | 
| 6 | 2, 5 | e1a 44647 | . . . . . . 7
⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶)   ▶   𝐴 ⊆ 𝐵   ) | 
| 7 |  | idn2 44633 | . . . . . . 7
⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶)   ,   𝑥 ∈ 𝐴   ▶   𝑥 ∈ 𝐴   ) | 
| 8 |  | ssel2 3978 | . . . . . . 7
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) | 
| 9 | 6, 7, 8 | e12an 44745 | . . . . . 6
⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶)   ,   𝑥 ∈ 𝐴   ▶   𝑥 ∈ 𝐵   ) | 
| 10 |  | ssel2 3978 | . . . . . 6
⊢ ((𝐵 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶) | 
| 11 | 4, 9, 10 | e12an 44745 | . . . . 5
⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶)   ,   𝑥 ∈ 𝐴   ▶   𝑥 ∈ 𝐶   ) | 
| 12 | 11 | in2 44625 | . . . 4
⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶)   ▶   (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)   ) | 
| 13 | 12 | gen11 44636 | . . 3
⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶)   ▶   ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)   ) | 
| 14 |  | biimpr 220 | . . 3
⊢ ((𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) → (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → 𝐴 ⊆ 𝐶)) | 
| 15 | 1, 13, 14 | e01 44711 | . 2
⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶)   ▶   𝐴 ⊆ 𝐶   ) | 
| 16 | 15 | in1 44591 | 1
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) |