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

Metamath Proof Explorer

Theorem rnmptssdf

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

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

Proof

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