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

Metamath Proof Explorer

Theorem ovex

Description: The result of an operation is a set. (Contributed by NM, 13-Mar-1995)

Ref Expression
Assertion ovex ( 𝐴 𝐹 𝐵 ) ∈ V

Proof

Step Hyp Ref Expression
1 df-ov ⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
2 1 fvexi ⊢ ( 𝐴 𝐹 𝐵 ) ∈ V