Description: Obsolete version of rnin as of 10-Jun-2026. (Contributed by NM, 15-Sep-2004) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rninOLD | ⊢ ran ( 𝐴 ∩ 𝐵 ) ⊆ ( ran 𝐴 ∩ ran 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnvin | ⊢ ◡ ( 𝐴 ∩ 𝐵 ) = ( ◡ 𝐴 ∩ ◡ 𝐵 ) | |
| 2 | 1 | dmeqi | ⊢ dom ◡ ( 𝐴 ∩ 𝐵 ) = dom ( ◡ 𝐴 ∩ ◡ 𝐵 ) |
| 3 | dmin | ⊢ dom ( ◡ 𝐴 ∩ ◡ 𝐵 ) ⊆ ( dom ◡ 𝐴 ∩ dom ◡ 𝐵 ) | |
| 4 | 2 3 | eqsstri | ⊢ dom ◡ ( 𝐴 ∩ 𝐵 ) ⊆ ( dom ◡ 𝐴 ∩ dom ◡ 𝐵 ) |
| 5 | df-rn | ⊢ ran ( 𝐴 ∩ 𝐵 ) = dom ◡ ( 𝐴 ∩ 𝐵 ) | |
| 6 | df-rn | ⊢ ran 𝐴 = dom ◡ 𝐴 | |
| 7 | df-rn | ⊢ ran 𝐵 = dom ◡ 𝐵 | |
| 8 | 6 7 | ineq12i | ⊢ ( ran 𝐴 ∩ ran 𝐵 ) = ( dom ◡ 𝐴 ∩ dom ◡ 𝐵 ) |
| 9 | 4 5 8 | 3sstr4i | ⊢ ran ( 𝐴 ∩ 𝐵 ) ⊆ ( ran 𝐴 ∩ ran 𝐵 ) |