Metamath Proof Explorer


Theorem ovex

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

Ref Expression
Assertion ovex AFBV

Proof

Step Hyp Ref Expression
1 df-ov AFB=FAB
2 1 fvexi AFBV