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

Metamath Proof Explorer

Theorem rnmptssd

Description: The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses rnmptssd.1 ⊢ Ⅎ x φ
rnmptssd.2 ⊢ F = x ∈ A ⟼ B
rnmptssd.3 ⊢ φ ∧ x ∈ A → B ∈ C
Assertion rnmptssd ⊢ φ → ran ⁡ F ⊆ C

Proof

Step Hyp Ref Expression
1 rnmptssd.1 ⊢ Ⅎ x φ
2 rnmptssd.2 ⊢ F = x ∈ A ⟼ B
3 rnmptssd.3 ⊢ φ ∧ x ∈ A → B ∈ C
4 1 3 ralrimia ⊢ φ → ∀ x ∈ A B ∈ C
5 2 rnmptss ⊢ ∀ x ∈ A B ∈ C → ran ⁡ F ⊆ C
6 4 5 syl ⊢ φ → ran ⁡ F ⊆ C