Metamath Proof Explorer

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 biimtrid 
 |-  ( A e. B -> ( x e. |^| B -> x e. A ) )
9 8 ssrdv 
 |-  ( A e. B -> |^| B C_ A )