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

Metamath Proof Explorer

Theorem fvmpt2bd

Description: Value of a function given by the maps-to notation. Deduction version. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Hypothesis	fvmpt2bd.1	$⊢ φ \to F = (x \in A ⟼ B)$
	Assertion	fvmpt2bd	$⊢ (φ \land x \in A \land B \in C) \to F (x) = B$

Step	Hyp	Ref	Expression
1		fvmpt2bd.1	$⊢ φ \to F = (x \in A ⟼ B)$
2	1	fveq1d	$⊢ φ \to F (x) = (x \in A ⟼ B) (x)$
3	2	3ad2ant1	$⊢ (φ \land x \in A \land B \in C) \to F (x) = (x \in A ⟼ B) (x)$
4		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
5	4	fvmpt2	$⊢ (x \in A \land B \in C) \to (x \in A ⟼ B) (x) = B$
6	5	3adant1	$⊢ (φ \land x \in A \land B \in C) \to (x \in A ⟼ B) (x) = B$
7	3 6	eqtrd	$⊢ (φ \land x \in A \land B \in C) \to F (x) = B$