dff2

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

		Ref	Expression
	Assertion	dff2	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land F \subseteq A \times B)$

Step	Hyp	Ref	Expression
1		ffn	$⊢ F : A ⟶ B \to F Fn A$
2		fssxp	$⊢ F : A ⟶ B \to F \subseteq A \times B$
3	1 2	jca	$⊢ F : A ⟶ B \to (F Fn A \land F \subseteq A \times B)$
4		rnss	$⊢ F \subseteq A \times B \to ran F \subseteq ran (A \times B)$
5		rnxpss	$⊢ ran (A \times B) \subseteq B$
6	4 5	sstrdi	$⊢ F \subseteq A \times B \to ran F \subseteq B$
7	6	anim2i	$⊢ (F Fn A \land F \subseteq A \times B) \to (F Fn A \land ran F \subseteq B)$
8		df-f	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land ran F \subseteq B)$
9	7 8	sylibr	$⊢ (F Fn A \land F \subseteq A \times B) \to F : A ⟶ B$
10	3 9	impbii	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land F \subseteq A \times B)$

Metamath Proof Explorer