This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imassrn

Description: The image of a class is a subset of its range. Theorem 3.16(xi) of Monk1 p. 39. (Contributed by NM, 31-Mar-1995)

Ref Expression
Assertion imassrn ⊢ A B ⊆ ran ⁡ A

Proof

Step Hyp Ref Expression
1 exsimpr ⊢ ∃ x x ∈ B ∧ x y ∈ A → ∃ x x y ∈ A
2 1 ss2abi ⊢ y | ∃ x x ∈ B ∧ x y ∈ A ⊆ y | ∃ x x y ∈ A
3 dfima3 ⊢ A B = y | ∃ x x ∈ B ∧ x y ∈ A
4 dfrn3 ⊢ ran ⁡ A = y | ∃ x x y ∈ A
5 2 3 4 3sstr4i ⊢ A B ⊆ ran ⁡ A