Metamath Proof Explorer

Theorem fvco2

Description: Value of a function composition. Similar to second part of Theorem 3H of Enderton p. 47. (Contributed by NM, 9-Oct-2004) (Proof shortened by Andrew Salmon, 22-Oct-2011) (Revised by Stefan O'Rear, 16-Oct-2014)

		Ref	Expression
	Assertion	fvco2	$⊢ (G Fn A \land X \in A) \to (F \circ G) (X) = F (G (X))$

Proof

Step	Hyp	Ref	Expression
1		fnsnfv	$⊢ (G Fn A \land X \in A) \to \{G (X)\} = G [\{X\}]$
2	1	imaeq2d	$⊢ (G Fn A \land X \in A) \to F [\{G (X)\}] = F [G [\{X\}]]$
3		imaco	$⊢ (F \circ G) [\{X\}] = F [G [\{X\}]]$
4	2 3	syl6reqr	$⊢ (G Fn A \land X \in A) \to (F \circ G) [\{X\}] = F [\{G (X)\}]$
5	4	eleq2d	$⊢ (G Fn A \land X \in A) \to (x \in (F \circ G) [\{X\}] \leftrightarrow x \in F [\{G (X)\}])$
6	5	iotabidv	$⊢ (G Fn A \land X \in A) \to (ι x \| x \in (F \circ G) [\{X\}]) = (ι x \| x \in F [\{G (X)\}])$
7		dffv3	$⊢ (F \circ G) (X) = (ι x \| x \in (F \circ G) [\{X\}])$
8		dffv3	$⊢ F (G (X)) = (ι x \| x \in F [\{G (X)\}])$
9	6 7 8	3eqtr4g	$⊢ (G Fn A \land X \in A) \to (F \circ G) (X) = F (G (X))$