Metamath Proof Explorer

Theorem sstskm

Description: Being a part of ( tarskiMapA ) . (Contributed by FL, 17-Apr-2011) (Proof shortened by Mario Carneiro, 20-Sep-2014)

Ref Expression
Assertion sstskm 
|- ( A e. V -> ( B C_ ( tarskiMap ` A ) <-> A. x e. Tarski ( A e. x -> B C_ x ) ) )

Proof

Step Hyp Ref Expression
1 tskmval 
 |-  ( A e. V -> ( tarskiMap ` A ) = |^| { x e. Tarski | A e. x } )
2 df-rab 
 |-  { x e. Tarski | A e. x } = { x | ( x e. Tarski /\ A e. x ) }
3 2 inteqi 
 |-  |^| { x e. Tarski | A e. x } = |^| { x | ( x e. Tarski /\ A e. x ) }
4 1 3 eqtrdi 
 |-  ( A e. V -> ( tarskiMap ` A ) = |^| { x | ( x e. Tarski /\ A e. x ) } )
5 4 sseq2d 
 |-  ( A e. V -> ( B C_ ( tarskiMap ` A ) <-> B C_ |^| { x | ( x e. Tarski /\ A e. x ) } ) )
6 impexp 
 |-  ( ( ( x e. Tarski /\ A e. x ) -> B C_ x ) <-> ( x e. Tarski -> ( A e. x -> B C_ x ) ) )
7 6 albii 
 |-  ( A. x ( ( x e. Tarski /\ A e. x ) -> B C_ x ) <-> A. x ( x e. Tarski -> ( A e. x -> B C_ x ) ) )
8 ssintab 
 |-  ( B C_ |^| { x | ( x e. Tarski /\ A e. x ) } <-> A. x ( ( x e. Tarski /\ A e. x ) -> B C_ x ) )
9 df-ral 
 |-  ( A. x e. Tarski ( A e. x -> B C_ x ) <-> A. x ( x e. Tarski -> ( A e. x -> B C_ x ) ) )
10 7 8 9 3bitr4i 
 |-  ( B C_ |^| { x | ( x e. Tarski /\ A e. x ) } <-> A. x e. Tarski ( A e. x -> B C_ x ) )
11 5 10 bitrdi 
 |-  ( A e. V -> ( B C_ ( tarskiMap ` A ) <-> A. x e. Tarski ( A e. x -> B C_ x ) ) )