# Metamath Proof Explorer

## Theorem ssin

Description: Subclass of intersection. Theorem 2.8(vii) of Monk1 p. 26. (Contributed by NM, 15-Jun-2004) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion ssin ${⊢}\left({A}\subseteq {B}\wedge {A}\subseteq {C}\right)↔{A}\subseteq {B}\cap {C}$

### Proof

Step Hyp Ref Expression
1 elin ${⊢}{x}\in \left({B}\cap {C}\right)↔\left({x}\in {B}\wedge {x}\in {C}\right)$
2 1 imbi2i ${⊢}\left({x}\in {A}\to {x}\in \left({B}\cap {C}\right)\right)↔\left({x}\in {A}\to \left({x}\in {B}\wedge {x}\in {C}\right)\right)$
3 2 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in \left({B}\cap {C}\right)\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({x}\in {B}\wedge {x}\in {C}\right)\right)$
4 jcab ${⊢}\left({x}\in {A}\to \left({x}\in {B}\wedge {x}\in {C}\right)\right)↔\left(\left({x}\in {A}\to {x}\in {B}\right)\wedge \left({x}\in {A}\to {x}\in {C}\right)\right)$
5 4 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({x}\in {B}\wedge {x}\in {C}\right)\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\to {x}\in {B}\right)\wedge \left({x}\in {A}\to {x}\in {C}\right)\right)$
6 19.26 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\to {x}\in {B}\right)\wedge \left({x}\in {A}\to {x}\in {C}\right)\right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {B}\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {C}\right)\right)$
7 3 5 6 3bitrri ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {B}\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {C}\right)\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in \left({B}\cap {C}\right)\right)$
8 dfss2 ${⊢}{A}\subseteq {B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {B}\right)$
9 dfss2 ${⊢}{A}\subseteq {C}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {C}\right)$
10 8 9 anbi12i ${⊢}\left({A}\subseteq {B}\wedge {A}\subseteq {C}\right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {B}\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {C}\right)\right)$
11 dfss2 ${⊢}{A}\subseteq {B}\cap {C}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in \left({B}\cap {C}\right)\right)$
12 7 10 11 3bitr4i ${⊢}\left({A}\subseteq {B}\wedge {A}\subseteq {C}\right)↔{A}\subseteq {B}\cap {C}$