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	⊢ ( 𝑥 = 𝐴 → ∃ 𝑦 𝑦 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ax6ev	⊢ ∃ 𝑦 𝑦 = 𝑥
2		eqeq2	⊢ ( 𝑥 = 𝐴 → ( 𝑦 = 𝑥 ↔ 𝑦 = 𝐴 ) )
3	2	biimpd	⊢ ( 𝑥 = 𝐴 → ( 𝑦 = 𝑥 → 𝑦 = 𝐴 ) )
4	3	eximdv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 𝑦 = 𝑥 → ∃ 𝑦 𝑦 = 𝐴 ) )
5	1 4	mpi	⊢ ( 𝑥 = 𝐴 → ∃ 𝑦 𝑦 = 𝐴 )