Theorem fnimapr

Description: The image of a pair under a function. (Contributed by Jeff Madsen, 6-Jan-2011)

	Ref	Expression
Assertion	fnimapr	$$⊢\left(FFnA\wedge B\in A\wedge C\in A\right)\to F\left[\left\{B,C\right\}\right]=\left\{F\left(B\right),F\left(C\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fnsnfv	$$⊢\left(FFnA\wedge B\in A\right)\to \left\{F\left(B\right)\right\}=F\left[\left\{B\right\}\right]$$
2	1	3adant3	$$⊢\left(FFnA\wedge B\in A\wedge C\in A\right)\to \left\{F\left(B\right)\right\}=F\left[\left\{B\right\}\right]$$
3		fnsnfv	$$⊢\left(FFnA\wedge C\in A\right)\to \left\{F\left(C\right)\right\}=F\left[\left\{C\right\}\right]$$
4	3	3adant2	$$⊢\left(FFnA\wedge B\in A\wedge C\in A\right)\to \left\{F\left(C\right)\right\}=F\left[\left\{C\right\}\right]$$
5	2 4	uneq12d	$$⊢\left(FFnA\wedge B\in A\wedge C\in A\right)\to \left\{F\left(B\right)\right\}\cup \left\{F\left(C\right)\right\}=F\left[\left\{B\right\}\right]\cup F\left[\left\{C\right\}\right]$$
6	5	eqcomd	$$⊢\left(FFnA\wedge B\in A\wedge C\in A\right)\to F\left[\left\{B\right\}\right]\cup F\left[\left\{C\right\}\right]=\left\{F\left(B\right)\right\}\cup \left\{F\left(C\right)\right\}$$
7		df-pr	$$⊢\left\{B,C\right\}=\left\{B\right\}\cup \left\{C\right\}$$
8	7	imaeq2i	$$⊢F\left[\left\{B,C\right\}\right]=F\left[\left\{B\right\}\cup \left\{C\right\}\right]$$
9		imaundi	$$⊢F\left[\left\{B\right\}\cup \left\{C\right\}\right]=F\left[\left\{B\right\}\right]\cup F\left[\left\{C\right\}\right]$$
10	8 9	eqtri	$$⊢F\left[\left\{B,C\right\}\right]=F\left[\left\{B\right\}\right]\cup F\left[\left\{C\right\}\right]$$
11		df-pr	$$⊢\left\{F\left(B\right),F\left(C\right)\right\}=\left\{F\left(B\right)\right\}\cup \left\{F\left(C\right)\right\}$$
12	6 10 11	3eqtr4g	$$⊢\left(FFnA\wedge B\in A\wedge C\in A\right)\to F\left[\left\{B,C\right\}\right]=\left\{F\left(B\right),F\left(C\right)\right\}$$