Theorem rp-abid

Description: Two ways to express a class. (Contributed by RP, 13-Feb-2025)

	Ref	Expression
Assertion	rp-abid	|- A = { x | E. a e. A x = a }

Proof

Step	Hyp	Ref	Expression
1		clel5	|- ( x e. A <-> E. a e. A x = a )
2	1	eqabi	|- A = { x | E. a e. A x = a }