Theorem wl-isseteq

Description: A class equal to a set variable implies it is a set. Note that A may be dependent on x . The consequent, resembling ax6ev , is the accepted expression for the idea of a class being a set. Sometimes a simpler expression like the antecedent here, or in elisset , is already sufficient to mark a class variable as a set. (Contributed by Wolf Lammen, 7-Sep-2025)

	Ref	Expression
Assertion	wl-isseteq	$$⊢x=A\to \exists yy=A$$

Proof

Step	Hyp	Ref	Expression
1		ax6ev	$$⊢\exists yy=x$$
2		eqeq2	$$⊢x=A\to \left(y=x\leftrightarrow y=A\right)$$
3	2	biimpd	$$⊢x=A\to \left(y=x\to y=A\right)$$
4	3	eximdv	$$⊢x=A\to \left(\exists yy=x\to \exists yy=A\right)$$
5	1 4	mpi	$$⊢x=A\to \exists yy=A$$