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

Metamath Proof Explorer

Theorem dmmpo

Description: 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 dmmpo ⊢ dom ⁡ F = A × B

Proof

Step Hyp Ref Expression
1 fmpo.1 ⊢ F = x ∈ A , y ∈ B ⟼ C
2 fnmpoi.2 ⊢ C ∈ V
3 1 2 fnmpoi ⊢ F Fn A × B
4 3 fndmi ⊢ dom ⁡ F = A × B