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 i^i B ) C_ ( ran A i^i ran B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | inss1 | |- ( A i^i B ) C_ A |
|
| 2 | 1 | rnssi | |- ran ( A i^i B ) C_ ran A |
| 3 | inss2 | |- ( A i^i B ) C_ B |
|
| 4 | 3 | rnssi | |- ran ( A i^i B ) C_ ran B |
| 5 | 2 4 | ssini | |- ran ( A i^i B ) C_ ( ran A i^i ran B ) |