Metamath Proof Explorer

Theorem fnfvof

Description: Function value of a pointwise composition. (Contributed by Stefan O'Rear, 5-Oct-2014) (Proof shortened by Mario Carneiro, 5-Jun-2015)

		Ref	Expression
	Assertion	fnfvof	$⊢ ((F Fn A \land G Fn A) \land (A \in V \land X \in A)) \to (F R_{f} G) (X) = F (X) R G (X)$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((F Fn A \land G Fn A) \land A \in V) \to F Fn A$
2		simplr	$⊢ ((F Fn A \land G Fn A) \land A \in V) \to G Fn A$
3		simpr	$⊢ ((F Fn A \land G Fn A) \land A \in V) \to A \in V$
4		inidm	$⊢ A \cap A = A$
5		eqidd	$⊢ (((F Fn A \land G Fn A) \land A \in V) \land X \in A) \to F (X) = F (X)$
6		eqidd	$⊢ (((F Fn A \land G Fn A) \land A \in V) \land X \in A) \to G (X) = G (X)$
7	1 2 3 3 4 5 6	ofval	$⊢ (((F Fn A \land G Fn A) \land A \in V) \land X \in A) \to (F R_{f} G) (X) = F (X) R G (X)$
8	7	anasss	$⊢ ((F Fn A \land G Fn A) \land (A \in V \land X \in A)) \to (F R_{f} G) (X) = F (X) R G (X)$