Metamath Proof Explorer

Theorem fvopabf4g

Description: Function value of an operator abstraction whose domain is a set of functions with given domain and range. (Contributed by Jeff Madsen, 1-Dec-2009) (Revised by Mario Carneiro, 12-Sep-2015)

		Ref	Expression
	Hypotheses	fvopabf4g.1	$⊢ C \in V$
		fvopabf4g.2	$⊢ x = A \to B = C$
		fvopabf4g.3	$⊢ F = (x \in (R^{D}) ⟼ B)$
	Assertion	fvopabf4g	$⊢ (D \in X \land R \in Y \land A : D ⟶ R) \to F (A) = C$

Proof

Step	Hyp	Ref	Expression
1		fvopabf4g.1	$⊢ C \in V$
2		fvopabf4g.2	$⊢ x = A \to B = C$
3		fvopabf4g.3	$⊢ F = (x \in (R^{D}) ⟼ B)$
4		elmapg	$⊢ (R \in Y \land D \in X) \to (A \in (R^{D}) \leftrightarrow A : D ⟶ R)$
5	4	ancoms	$⊢ (D \in X \land R \in Y) \to (A \in (R^{D}) \leftrightarrow A : D ⟶ R)$
6	5	biimp3ar	$⊢ (D \in X \land R \in Y \land A : D ⟶ R) \to A \in (R^{D})$
7	2 3 1	fvmpt	$⊢ A \in (R^{D}) \to F (A) = C$
8	6 7	syl	$⊢ (D \in X \land R \in Y \land A : D ⟶ R) \to F (A) = C$