Theorem encv

Description: If two classes are equinumerous, both classes are sets. (Contributed by AV, 21-Mar-2019)

	Ref	Expression
Assertion	encv	$$⊢A\approx B\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		relen	$$⊢\mathrm{Rel}\approx$$
2	1	brrelex12i	$$⊢A\approx B\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$