Description: An element of a class includes the intersection of the class. Exercise 4 of TakeutiZaring p. 44 (with correction), generalized to classes. (Contributed by NM, 18-Nov-1995)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | intss1 | ⊢ ( 𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex | ⊢ 𝑥 ∈ V | |
| 2 | 1 | elint | ⊢ ( 𝑥 ∈ ∩ 𝐵 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦 ) ) |
| 3 | eleq1 | ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) ) | |
| 4 | eleq2 | ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴 ) ) | |
| 5 | 3 4 | imbi12d | ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦 ) ↔ ( 𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴 ) ) ) |
| 6 | 5 | spcgv | ⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦 ) → ( 𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴 ) ) ) |
| 7 | 6 | pm2.43a | ⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦 ) → 𝑥 ∈ 𝐴 ) ) |
| 8 | 2 7 | biimtrid | ⊢ ( 𝐴 ∈ 𝐵 → ( 𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴 ) ) |
| 9 | 8 | ssrdv | ⊢ ( 𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴 ) |