This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fmpo

Description: Functionality, domain and range of a class given by the maps-to notation. (Contributed by FL, 17-May-2010)

		Ref	Expression
	Hypothesis	fmpo.1	$⊢ F = (x \in A, y \in B ⟼ C)$
	Assertion	fmpo	$⊢ \forall x \in A \forall y \in B C \in D \leftrightarrow F : A \times B ⟶ D$

Step	Hyp	Ref	Expression
1		fmpo.1	$⊢ F = (x \in A, y \in B ⟼ C)$
2	1	fmpox	$⊢ \forall x \in A \forall y \in B C \in D \leftrightarrow F : ⋃_{x \in A} (\{x\} \times B) ⟶ D$
3		iunxpconst	$⊢ ⋃_{x \in A} (\{x\} \times B) = A \times B$
4	3	feq2i	$⊢ F : ⋃_{x \in A} (\{x\} \times B) ⟶ D \leftrightarrow F : A \times B ⟶ D$
5	2 4	bitri	$⊢ \forall x \in A \forall y \in B C \in D \leftrightarrow F : A \times B ⟶ D$