This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( A C_ B /\ A C_ C ) <-> A C_ ( B i^i C ) )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
2 1 imbi2i 
 |-  ( ( x e. A -> x e. ( B i^i C ) ) <-> ( x e. A -> ( x e. B /\ x e. C ) ) )
3 2 albii 
 |-  ( A. x ( x e. A -> x e. ( B i^i C ) ) <-> A. x ( x e. A -> ( x e. B /\ x e. C ) ) )
4 jcab 
 |-  ( ( x e. A -> ( x e. B /\ x e. C ) ) <-> ( ( x e. A -> x e. B ) /\ ( x e. A -> x e. C ) ) )
5 4 albii 
 |-  ( A. x ( x e. A -> ( x e. B /\ x e. C ) ) <-> A. x ( ( x e. A -> x e. B ) /\ ( x e. A -> x e. C ) ) )
6 19.26 
 |-  ( A. x ( ( x e. A -> x e. B ) /\ ( x e. A -> x e. C ) ) <-> ( A. x ( x e. A -> x e. B ) /\ A. x ( x e. A -> x e. C ) ) )
7 3 5 6 3bitrri 
 |-  ( ( A. x ( x e. A -> x e. B ) /\ A. x ( x e. A -> x e. C ) ) <-> A. x ( x e. A -> x e. ( B i^i C ) ) )
8 df-ss 
 |-  ( A C_ B <-> A. x ( x e. A -> x e. B ) )
9 df-ss 
 |-  ( A C_ C <-> A. x ( x e. A -> x e. C ) )
10 8 9 anbi12i 
 |-  ( ( A C_ B /\ A C_ C ) <-> ( A. x ( x e. A -> x e. B ) /\ A. x ( x e. A -> x e. C ) ) )
11 df-ss 
 |-  ( A C_ ( B i^i C ) <-> A. x ( x e. A -> x e. ( B i^i C ) ) )
12 7 10 11 3bitr4i 
 |-  ( ( A C_ B /\ A C_ C ) <-> A C_ ( B i^i C ) )