Theorem intss

Description: Intersection of subclasses. (Contributed by NM, 14-Oct-1999) (Proof shortened by OpenAI, 25-Mar-2020)

	Ref	Expression
Assertion	intss	⊢ ( 𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssralv	⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 → ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 ) )
2	1	ss2abdv	⊢ ( 𝐴 ⊆ 𝐵 → { 𝑦 ∣ ∀ 𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 } ⊆ { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 } )
3		dfint2	⊢ ∩ 𝐵 = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 }
4		dfint2	⊢ ∩ 𝐴 = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 }
5	2 3 4	3sstr4g	⊢ ( 𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴 )