Metamath Proof Explorer


Theorem rnin

Description: The range of an intersection belongs the intersection of ranges. Theorem 9 of Suppes p. 60. (Contributed by NM, 15-Sep-2004) Avoid ax-pr and ax-sep . (Revised by Umit Teoman Dogan, 10-Jun-2026)

Ref Expression
Assertion rnin ⊢ ran ⁡ A ∩ B ⊆ ran ⁡ A ∩ ran ⁡ B

Proof

Step Hyp Ref Expression
1 inss1 ⊢ A ∩ B ⊆ A
2 1 rnssi ⊢ ran ⁡ A ∩ B ⊆ ran ⁡ A
3 inss2 ⊢ A ∩ B ⊆ B
4 3 rnssi ⊢ ran ⁡ A ∩ B ⊆ ran ⁡ B
5 2 4 ssini ⊢ ran ⁡ A ∩ B ⊆ ran ⁡ A ∩ ran ⁡ B