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 )