Theorem fmptpr

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

	Ref	Expression
Hypotheses	fmptpr.1	|- ( ph -> A e. V )
	fmptpr.2	|- ( ph -> B e. W )
	fmptpr.3	|- ( ph -> C e. X )
	fmptpr.4	|- ( ph -> D e. Y )
	fmptpr.5	|- ( ( ph /\ x = A ) -> E = C )
	fmptpr.6	|- ( ( ph /\ x = B ) -> E = D )
Assertion	fmptpr	|- ( ph -> { <. A , C >. , <. B , D >. } = ( x e. { A , B } |-> E ) )

Proof

Step	Hyp	Ref	Expression
1		fmptpr.1	|- ( ph -> A e. V )
2		fmptpr.2	|- ( ph -> B e. W )
3		fmptpr.3	|- ( ph -> C e. X )
4		fmptpr.4	|- ( ph -> D e. Y )
5		fmptpr.5	|- ( ( ph /\ x = A ) -> E = C )
6		fmptpr.6	|- ( ( ph /\ x = B ) -> E = D )
7		df-pr	|- { <. A , C >. , <. B , D >. } = ( { <. A , C >. } u. { <. B , D >. } )
8	7	a1i	|- ( ph -> { <. A , C >. , <. B , D >. } = ( { <. A , C >. } u. { <. B , D >. } ) )
9	5 1 3	fmptsnd	|- ( ph -> { <. A , C >. } = ( x e. { A } |-> E ) )
10	9	uneq1d	|- ( ph -> ( { <. A , C >. } u. { <. B , D >. } ) = ( ( x e. { A } |-> E ) u. { <. B , D >. } ) )
11		df-pr	|- { A , B } = ( { A } u. { B } )
12	11	eqcomi	|- ( { A } u. { B } ) = { A , B }
13	12	a1i	|- ( ph -> ( { A } u. { B } ) = { A , B } )
14	2 4 13 6	fmptapd	|- ( ph -> ( ( x e. { A } |-> E ) u. { <. B , D >. } ) = ( x e. { A , B } |-> E ) )
15	8 10 14	3eqtrd	|- ( ph -> { <. A , C >. , <. B , D >. } = ( x e. { A , B } |-> E ) )