# Metamath Proof Explorer

## Theorem ssel

Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993) Avoid ax-12 . (Revised by SN, 27-May-2024)

Ref Expression
Assertion ssel ${⊢}{A}\subseteq {B}\to \left({C}\in {A}\to {C}\in {B}\right)$

### Proof

Step Hyp Ref Expression
1 dfss2 ${⊢}{A}\subseteq {B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {B}\right)$
2 id ${⊢}\left({x}\in {A}\to {x}\in {B}\right)\to \left({x}\in {A}\to {x}\in {B}\right)$
3 2 anim2d ${⊢}\left({x}\in {A}\to {x}\in {B}\right)\to \left(\left({x}={C}\wedge {x}\in {A}\right)\to \left({x}={C}\wedge {x}\in {B}\right)\right)$
4 3 aleximi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {B}\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={C}\wedge {x}\in {A}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={C}\wedge {x}\in {B}\right)\right)$
5 dfclel ${⊢}{C}\in {A}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={C}\wedge {x}\in {A}\right)$
6 dfclel ${⊢}{C}\in {B}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={C}\wedge {x}\in {B}\right)$
7 4 5 6 3imtr4g ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {B}\right)\to \left({C}\in {A}\to {C}\in {B}\right)$
8 1 7 sylbi ${⊢}{A}\subseteq {B}\to \left({C}\in {A}\to {C}\in {B}\right)$