Theorem encv

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

	Ref	Expression
Assertion	encv	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		relen	⊢ Rel ≈
2	1	brrelex12i	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )