Metamath Proof Explorer

Theorem brovmpoex

Description: A binary relation of the value of an operation given by the maps-to notation. (Contributed by Alexander van der Vekens, 21-Oct-2017)

Ref Expression
Hypothesis brovmpoex.1 ⊢ O = x ∈ V , y ∈ V ⟼ z w | φ
Assertion brovmpoex ⊢ F V O E P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V

Proof

Step Hyp Ref Expression
1 brovmpoex.1 ⊢ O = x ∈ V , y ∈ V ⟼ z w | φ
2 1 relmpoopab ⊢ Rel ⁡ V O E
3 2 a1i ⊢ V ∈ V ∧ E ∈ V → Rel ⁡ V O E
4 1 3 brovex ⊢ F V O E P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V