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

Metamath Proof Explorer

Theorem rnmptc

Description: Range of a constant function in maps-to notation. (Contributed by Glauco Siliprandi, 11-Dec-2019) Remove extra hypothesis. (Revised by SN, 17-Apr-2024)

	Ref	Expression
Hypotheses	rnmptc.f	$⊢ F = (x \in A ⟼ B)$
	rnmptc.a	$⊢ φ \to A \neq \emptyset$
Assertion	rnmptc	$⊢ φ \to ran F = \{B\}$

Proof

Step	Hyp	Ref	Expression
1		rnmptc.f	$⊢ F = (x \in A ⟼ B)$
2		rnmptc.a	$⊢ φ \to A \neq \emptyset$
3		fconstmpt	$⊢ A \times \{B\} = (x \in A ⟼ B)$
4	1 3	eqtr4i	$⊢ F = A \times \{B\}$
5	4	rneqi	$⊢ ran F = ran (A \times \{B\})$
6		rnxp	$⊢ A \neq \emptyset \to ran (A \times \{B\}) = \{B\}$
7	5 6	eqtrid	$⊢ A \neq \emptyset \to ran F = \{B\}$
8	2 7	syl	$⊢ φ \to ran F = \{B\}$