dff4

Description: Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007)

		Ref	Expression
	Assertion	dff4	$⊢ F : A ⟶ B \leftrightarrow (F \subseteq A \times B \land \forall x \in A \exists! y \in B x F y)$

Step	Hyp	Ref	Expression
1		dff3	$⊢ F : A ⟶ B \leftrightarrow (F \subseteq A \times B \land \forall x \in A \exists! y x F y)$
2		df-br	$⊢ x F y \leftrightarrow ⟨x, y⟩ \in F$
3		ssel	$⊢ F \subseteq A \times B \to (⟨x, y⟩ \in F \to ⟨x, y⟩ \in (A \times B))$
4		opelxp2	$⊢ ⟨x, y⟩ \in (A \times B) \to y \in B$
5	3 4	syl6	$⊢ F \subseteq A \times B \to (⟨x, y⟩ \in F \to y \in B)$
6	2 5	syl5bi	$⊢ F \subseteq A \times B \to (x F y \to y \in B)$
7	6	pm4.71rd	$⊢ F \subseteq A \times B \to (x F y \leftrightarrow (y \in B \land x F y))$
8	7	eubidv	$⊢ F \subseteq A \times B \to (\exists! y x F y \leftrightarrow \exists! y (y \in B \land x F y))$
9		df-reu	$⊢ \exists! y \in B x F y \leftrightarrow \exists! y (y \in B \land x F y)$
10	8 9	bitr4di	$⊢ F \subseteq A \times B \to (\exists! y x F y \leftrightarrow \exists! y \in B x F y)$
11	10	ralbidv	$⊢ F \subseteq A \times B \to (\forall x \in A \exists! y x F y \leftrightarrow \forall x \in A \exists! y \in B x F y)$
12	11	pm5.32i	$⊢ (F \subseteq A \times B \land \forall x \in A \exists! y x F y) \leftrightarrow (F \subseteq A \times B \land \forall x \in A \exists! y \in B x F y)$
13	1 12	bitri	$⊢ F : A ⟶ B \leftrightarrow (F \subseteq A \times B \land \forall x \in A \exists! y \in B x F y)$

Metamath Proof Explorer