Description: Obsolete version of imassrn as of 27-Sep-2026. (Contributed by NM, 31-Mar-1995) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | imassrnOLD | ⊢ ( 𝐴 “ 𝐵 ) ⊆ ran 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exsimpr | ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) → ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) | |
| 2 | 1 | ss2abi | ⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) } ⊆ { 𝑦 ∣ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } |
| 3 | dfima3 | ⊢ ( 𝐴 “ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) } | |
| 4 | dfrn3 | ⊢ ran 𝐴 = { 𝑦 ∣ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } | |
| 5 | 2 3 4 | 3sstr4i | ⊢ ( 𝐴 “ 𝐵 ) ⊆ ran 𝐴 |