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\to A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2		eleq1	$$⊢x=A\to \left(x\in \mathrm{V}\leftrightarrow A\in \mathrm{V}\right)$$
3	1 2	mpbii	$$⊢x=A\to A\in \mathrm{V}$$