This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tskin

Description: The intersection of two elements of a Tarski class belongs to the class. (Contributed by FL, 30-Dec-2010) (Proof shortened by Mario Carneiro, 20-Sep-2014)

Ref Expression
Assertion tskin ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝑇 )

Proof

Step Hyp Ref Expression
1 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
2 tskss ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝑇 )
3 1 2 mp3an3 ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝑇 )