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

Metamath Proof Explorer

Theorem rnmptssdff

Description: The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 24-Jan-2025)

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

Proof

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