Metamath Proof Explorer

Theorem encv

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

Ref Expression
Assertion encv 
|- ( A ~~ B -> ( A e. _V /\ B e. _V ) )

Proof

Step Hyp Ref Expression
1 relen 
 |-  Rel ~~
2 1 brrelex12i 
 |-  ( A ~~ B -> ( A e. _V /\ B e. _V ) )