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 -> E. y y = A )

Proof

Step	Hyp	Ref	Expression
1		ax6ev	|- E. y y = x
2		eqeq2	|- ( x = A -> ( y = x <-> y = A ) )
3	2	biimpd	|- ( x = A -> ( y = x -> y = A ) )
4	3	eximdv	|- ( x = A -> ( E. y y = x -> E. y y = A ) )
5	1 4	mpi	|- ( x = A -> E. y y = A )