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	⊢ ( 𝑥 = 𝐴 → 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ V ↔ 𝐴 ∈ V ) )
3	1 2	mpbii	⊢ ( 𝑥 = 𝐴 → 𝐴 ∈ V )