fssxp

Description: A mapping is a class of ordered pairs. (Contributed by NM, 3-Aug-1994) (Proof shortened by Andrew Salmon, 17-Sep-2011)

		Ref	Expression
	Assertion	fssxp	$⊢ F : A ⟶ B \to F \subseteq A \times B$

Step	Hyp	Ref	Expression
1		frel	$⊢ F : A ⟶ B \to Rel F$
2		relssdmrn	$⊢ Rel F \to F \subseteq dom F \times ran F$
3	1 2	syl	$⊢ F : A ⟶ B \to F \subseteq dom F \times ran F$
4		fdm	$⊢ F : A ⟶ B \to dom F = A$
5		eqimss	$⊢ dom F = A \to dom F \subseteq A$
6	4 5	syl	$⊢ F : A ⟶ B \to dom F \subseteq A$
7		frn	$⊢ F : A ⟶ B \to ran F \subseteq B$
8		xpss12	$⊢ (dom F \subseteq A \land ran F \subseteq B) \to dom F \times ran F \subseteq A \times B$
9	6 7 8	syl2anc	$⊢ F : A ⟶ B \to dom F \times ran F \subseteq A \times B$
10	3 9	sstrd	$⊢ F : A ⟶ B \to F \subseteq A \times B$

Metamath Proof Explorer