Metamath Proof Explorer

Theorem elovmpt3rab

Description: Implications for the value of an operation defined by the maps-to notation with a class abstraction as a result having an element. (Contributed by AV, 17-Jul-2018) (Revised by AV, 16-May-2019)

Ref Expression
Hypothesis elovmpt3rab.o ⊢ O = x ∈ V , y ∈ V ⟼ z ∈ M ⟼ a ∈ N | φ
Assertion elovmpt3rab ⊢ M ∈ U ∧ N ∈ T → A ∈ X O Y ⁡ Z → X ∈ V ∧ Y ∈ V ∧ Z ∈ M ∧ A ∈ N

Proof

Step Hyp Ref Expression
1 elovmpt3rab.o ⊢ O = x ∈ V , y ∈ V ⟼ z ∈ M ⟼ a ∈ N | φ
2 eqidd ⊢ x = X ∧ y = Y → M = M
3 eqidd ⊢ x = X ∧ y = Y → N = N
4 1 2 3 elovmpt3rab1 ⊢ M ∈ U ∧ N ∈ T → A ∈ X O Y ⁡ Z → X ∈ V ∧ Y ∈ V ∧ Z ∈ M ∧ A ∈ N