Theorem ovexi

Description: The result of an operation is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypothesis	ovexi.1	$$⊢A=BFC$$
Assertion	ovexi	$$⊢A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ovexi.1	$$⊢A=BFC$$
2		ovex	$$⊢BFC\in \mathrm{V}$$
3	1 2	eqeltri	$$⊢A\in \mathrm{V}$$