Metamath Proof Explorer

Theorem mpoexga

Description: If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by NM, 12-Sep-2011)

Ref Expression
Assertion mpoexga ⊢ A ∈ V ∧ B ∈ W → x ∈ A , y ∈ B ⟼ C ∈ V

Proof

Step Hyp Ref Expression
1 eqid ⊢ x ∈ A , y ∈ B ⟼ C = x ∈ A , y ∈ B ⟼ C
2 1 mpoexg ⊢ A ∈ V ∧ B ∈ W → x ∈ A , y ∈ B ⟼ C ∈ V