Theorem funpr

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

	Ref	Expression
Hypotheses	funpr.1	$$⊢A\in \mathrm{V}$$
	funpr.2	$$⊢B\in \mathrm{V}$$
	funpr.3	$$⊢C\in \mathrm{V}$$
	funpr.4	$$⊢D\in \mathrm{V}$$
Assertion	funpr	$$⊢A\ne B\to \mathrm{Fun}\left\{⟨A,C⟩,⟨B,D⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		funpr.1	$$⊢A\in \mathrm{V}$$
2		funpr.2	$$⊢B\in \mathrm{V}$$
3		funpr.3	$$⊢C\in \mathrm{V}$$
4		funpr.4	$$⊢D\in \mathrm{V}$$
5	1 2	pm3.2i	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
6	3 4	pm3.2i	$$⊢\left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)$$
7		funprg	$$⊢\left(\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\wedge \left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)\wedge A\ne B\right)\to \mathrm{Fun}\left\{⟨A,C⟩,⟨B,D⟩\right\}$$
8	5 6 7	mp3an12	$$⊢A\ne B\to \mathrm{Fun}\left\{⟨A,C⟩,⟨B,D⟩\right\}$$