Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sseli.1 | ⊢ 𝐴 ⊆ 𝐵 | |
sseldi.2 | ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 ) | ||
Assertion | sseldi | ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseli.1 | ⊢ 𝐴 ⊆ 𝐵 | |
2 | sseldi.2 | ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 ) | |
3 | 1 | sseli | ⊢ ( 𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) |
4 | 2 3 | syl | ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 ) |