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∈V→B⊆tarskiMap⁡A↔∀x∈TarskiA∈x→B⊆x

Proof

Step Hyp Ref Expression
1 tskmval ⊢A∈V→tarskiMap⁡A=⋂x∈Tarski|A∈x
2 df-rab ⊢x∈Tarski|A∈x=x|x∈Tarski∧A∈x
3 2 inteqi ⊢⋂x∈Tarski|A∈x=⋂x|x∈Tarski∧A∈x
4 1 3 eqtrdi ⊢A∈V→tarskiMap⁡A=⋂x|x∈Tarski∧A∈x
5 4 sseq2d ⊢A∈V→B⊆tarskiMap⁡A↔B⊆⋂x|x∈Tarski∧A∈x
6 impexp ⊢x∈Tarski∧A∈x→B⊆x↔x∈Tarski→A∈x→B⊆x
7 6 albii ⊢∀xx∈Tarski∧A∈x→B⊆x↔∀xx∈Tarski→A∈x→B⊆x
8 ssintab ⊢B⊆⋂x|x∈Tarski∧A∈x↔∀xx∈Tarski∧A∈x→B⊆x
9 df-ral ⊢∀x∈TarskiA∈x→B⊆x↔∀xx∈Tarski→A∈x→B⊆x
10 7 8 9 3bitr4i ⊢B⊆⋂x|x∈Tarski∧A∈x↔∀x∈TarskiA∈x→B⊆x
11 5 10 bitrdi ⊢A∈V→B⊆tarskiMap⁡A↔∀x∈TarskiA∈x→B⊆x