Theorem funpr

Description: A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010)

	Ref	Expression
Hypotheses	funpr.1	|- A e. _V
	funpr.2	|- B e. _V
	funpr.3	|- C e. _V
	funpr.4	|- D e. _V
Assertion	funpr	|- ( A =/= B -> Fun { <. A , C >. , <. B , D >. } )

Proof

Step	Hyp	Ref	Expression
1		funpr.1	|- A e. _V
2		funpr.2	|- B e. _V
3		funpr.3	|- C e. _V
4		funpr.4	|- D e. _V
5	1 2	pm3.2i	|- ( A e. _V /\ B e. _V )
6	3 4	pm3.2i	|- ( C e. _V /\ D e. _V )
7		funprg	|- ( ( ( A e. _V /\ B e. _V ) /\ ( C e. _V /\ D e. _V ) /\ A =/= B ) -> Fun { <. A , C >. , <. B , D >. } )
8	5 6 7	mp3an12	|- ( A =/= B -> Fun { <. A , C >. , <. B , D >. } )