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

Metamath Proof Explorer

Theorem fvconst2

Description: The value of a constant function. (Contributed by NM, 16-Apr-2005)

		Ref	Expression
	Hypothesis	fvconst2.1	$⊢ B \in V$
	Assertion	fvconst2	$⊢ C \in A \to (A \times \{B\}) (C) = B$

Step	Hyp	Ref	Expression
1		fvconst2.1	$⊢ B \in V$
2		fvconst2g	$⊢ (B \in V \land C \in A) \to (A \times \{B\}) (C) = B$
3	1 2	mpan	$⊢ C \in A \to (A \times \{B\}) (C) = B$