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

Metamath Proof Explorer

Theorem mpoex

Description: If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by Mario Carneiro, 20-Dec-2013)

Ref Expression
Hypotheses mpoex.1 ⊢ A ∈ V
mpoex.2 ⊢ B ∈ V
Assertion mpoex ⊢ x ∈ A , y ∈ B ⟼ C ∈ V

Proof

Step Hyp Ref Expression
1 mpoex.1 ⊢ A ∈ V
2 mpoex.2 ⊢ B ∈ V
3 2 rgenw ⊢ ∀ x ∈ A B ∈ V
4 eqid ⊢ x ∈ A , y ∈ B ⟼ C = x ∈ A , y ∈ B ⟼ C
5 4 mpoexxg ⊢ A ∈ V ∧ ∀ x ∈ A B ∈ V → x ∈ A , y ∈ B ⟼ C ∈ V
6 1 3 5 mp2an ⊢ x ∈ A , y ∈ B ⟼ C ∈ V