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

Metamath Proof Explorer

Theorem ssint

Description: Subclass of a class intersection. Theorem 5.11(viii) of Monk1 p. 52 and its converse. (Contributed by NM, 14-Oct-1999)

Ref Expression
Assertion ssint 
|- ( A C_ |^| B <-> A. x e. B A C_ x )

Proof

Step Hyp Ref Expression
1 dfss3 
 |-  ( A C_ |^| B <-> A. y e. A y e. |^| B )
2 vex 
 |-  y e. _V
3 2 elint2 
 |-  ( y e. |^| B <-> A. x e. B y e. x )
4 3 ralbii 
 |-  ( A. y e. A y e. |^| B <-> A. y e. A A. x e. B y e. x )
5 ralcom 
 |-  ( A. y e. A A. x e. B y e. x <-> A. x e. B A. y e. A y e. x )
6 dfss3 
 |-  ( A C_ x <-> A. y e. A y e. x )
7 6 ralbii 
 |-  ( A. x e. B A C_ x <-> A. x e. B A. y e. A y e. x )
8 5 7 bitr4i 
 |-  ( A. y e. A A. x e. B y e. x <-> A. x e. B A C_ x )
9 1 4 8 3bitri 
 |-  ( A C_ |^| B <-> A. x e. B A C_ x )