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

Metamath Proof Explorer

Theorem fnmpoi

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

Ref Expression
Hypotheses fmpo.1 ⊢ F = x ∈ A , y ∈ B ⟼ C
fnmpoi.2 ⊢ C ∈ V
Assertion fnmpoi ⊢ F Fn A × B

Proof

Step Hyp Ref Expression
1 fmpo.1 ⊢ F = x ∈ A , y ∈ B ⟼ C
2 fnmpoi.2 ⊢ C ∈ V
3 2 rgen2w ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V
4 1 fnmpo ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V → F Fn A × B
5 3 4 ax-mp ⊢ F Fn A × B