Description: Obsolete version of ssel as of 27-May-2024. (Contributed by NM, 5-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sselOLD | ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfss2 | ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) | |
| 2 | 1 | biimpi | ⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) |
| 3 | 2 | 19.21bi | ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) |
| 4 | 3 | anim2d | ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵 ) ) ) |
| 5 | 4 | eximdv | ⊢ ( 𝐴 ⊆ 𝐵 → ( ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵 ) ) ) |
| 6 | dfclel | ⊢ ( 𝐶 ∈ 𝐴 ↔ ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴 ) ) | |
| 7 | dfclel | ⊢ ( 𝐶 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵 ) ) | |
| 8 | 5 6 7 | 3imtr4g | ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) ) |