Slate - Intersection is subset of left argument

Library ▹ Essentials ▹ Sets

Proposition 1.1.12. Let U be a set, S, T ⊆ U. Then:

Proof. Let x ∈ S ∩ T.

⇒^def x ∈ S

References.

https://proofwiki.org/wiki/Intersection_is_Subset
http://metamath.tirix.org/inss1.html
https://leanprover-community.github.io/mathlib_docs/data/set/basic.html#set.inter_subset_left