fnprg

Description: Function with a domain of two different values. (Contributed by FL, 26-Jun-2011) (Revised by Mario Carneiro, 26-Apr-2015)

		Ref	Expression
	Assertion	fnprg	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y) \land A \neq B) \to \{⟨A, C⟩, ⟨B, D⟩\} Fn \{A, B\}$

Step	Hyp	Ref	Expression
1		funprg	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y) \land A \neq B) \to Fun \{⟨A, C⟩, ⟨B, D⟩\}$
2		dmpropg	$⊢ (C \in X \land D \in Y) \to dom \{⟨A, C⟩, ⟨B, D⟩\} = \{A, B\}$
3	2	3ad2ant2	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y) \land A \neq B) \to dom \{⟨A, C⟩, ⟨B, D⟩\} = \{A, B\}$
4		df-fn	$⊢ \{⟨A, C⟩, ⟨B, D⟩\} Fn \{A, B\} \leftrightarrow (Fun \{⟨A, C⟩, ⟨B, D⟩\} \land dom \{⟨A, C⟩, ⟨B, D⟩\} = \{A, B\})$
5	1 3 4	sylanbrc	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y) \land A \neq B) \to \{⟨A, C⟩, ⟨B, D⟩\} Fn \{A, B\}$

Metamath Proof Explorer