Theorem fmptpr

Description: Express a pair function in maps-to notation. (Contributed by Thierry Arnoux, 3-Jan-2017)

	Ref	Expression
Hypotheses	fmptpr.1	$$⊢\phi \to A\in V$$
	fmptpr.2	$$⊢\phi \to B\in W$$
	fmptpr.3	$$⊢\phi \to C\in X$$
	fmptpr.4	$$⊢\phi \to D\in Y$$
	fmptpr.5	$$⊢\left(\phi \wedge x=A\right)\to E=C$$
	fmptpr.6	$$⊢\left(\phi \wedge x=B\right)\to E=D$$
Assertion	fmptpr	$$⊢\phi \to \left\{⟨A,C⟩,⟨B,D⟩\right\}=\left(x\in \left\{A,B\right\}⟼E\right)$$

Proof

Step	Hyp	Ref	Expression
1		fmptpr.1	$$⊢\phi \to A\in V$$
2		fmptpr.2	$$⊢\phi \to B\in W$$
3		fmptpr.3	$$⊢\phi \to C\in X$$
4		fmptpr.4	$$⊢\phi \to D\in Y$$
5		fmptpr.5	$$⊢\left(\phi \wedge x=A\right)\to E=C$$
6		fmptpr.6	$$⊢\left(\phi \wedge x=B\right)\to E=D$$
7		df-pr	$$⊢\left\{⟨A,C⟩,⟨B,D⟩\right\}=\left\{⟨A,C⟩\right\}\cup \left\{⟨B,D⟩\right\}$$
8	7	a1i	$$⊢\phi \to \left\{⟨A,C⟩,⟨B,D⟩\right\}=\left\{⟨A,C⟩\right\}\cup \left\{⟨B,D⟩\right\}$$
9	5 1 3	fmptsnd	$$⊢\phi \to \left\{⟨A,C⟩\right\}=\left(x\in \left\{A\right\}⟼E\right)$$
10	9	uneq1d	$$⊢\phi \to \left\{⟨A,C⟩\right\}\cup \left\{⟨B,D⟩\right\}=\left(x\in \left\{A\right\}⟼E\right)\cup \left\{⟨B,D⟩\right\}$$
11		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
12	11	eqcomi	$$⊢\left\{A\right\}\cup \left\{B\right\}=\left\{A,B\right\}$$
13	12	a1i	$$⊢\phi \to \left\{A\right\}\cup \left\{B\right\}=\left\{A,B\right\}$$
14	2 4 13 6	fmptapd	$$⊢\phi \to \left(x\in \left\{A\right\}⟼E\right)\cup \left\{⟨B,D⟩\right\}=\left(x\in \left\{A,B\right\}⟼E\right)$$
15	8 10 14	3eqtrd	$$⊢\phi \to \left\{⟨A,C⟩,⟨B,D⟩\right\}=\left(x\in \left\{A,B\right\}⟼E\right)$$