Metamath Proof Explorer

Theorem eqvisset

Description: A class equal to a variable is a set. Note the absence of disjoint variable condition, contrary to isset and issetri . (Contributed by BJ, 27-Apr-2019)

Ref Expression
Assertion eqvisset x = A A V


Step Hyp Ref Expression
1 vex x V
2 eleq1 x = A x V A V
3 1 2 mpbii x = A A V