Theorem intss1

Description: An element of a class includes the intersection of the class. Exercise 4 of TakeutiZaring p. 44 (with correction), generalized to classes. (Contributed by NM, 18-Nov-1995)

	Ref	Expression
Assertion	intss1	|- ( A e. B -> |^| B C_ A )

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	elint	|- ( x e. |^| B <-> A. y ( y e. B -> x e. y ) )
3		eleq1	|- ( y = A -> ( y e. B <-> A e. B ) )
4		eleq2	|- ( y = A -> ( x e. y <-> x e. A ) )
5	3 4	imbi12d	|- ( y = A -> ( ( y e. B -> x e. y ) <-> ( A e. B -> x e. A ) ) )
6	5	spcgv	|- ( A e. B -> ( A. y ( y e. B -> x e. y ) -> ( A e. B -> x e. A ) ) )
7	6	pm2.43a	|- ( A e. B -> ( A. y ( y e. B -> x e. y ) -> x e. A ) )
8	2 7	syl5bi	|- ( A e. B -> ( x e. |^| B -> x e. A ) )
9	8	ssrdv	|- ( A e. B -> |^| B C_ A )