Theorem clel5OLD

Description: Obsolete version of clel5 as of 19-May-2023. Alternate definition of class membership: a class X is an element of another class A iff there is an element of A equal to X . (Contributed by AV, 13-Nov-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	clel5OLD	$$⊢X\in A\leftrightarrow \exists x\in AX=x$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢X\in A\to X\in A$$
2		eqeq2	$$⊢x=X\to \left(X=x\leftrightarrow X=X\right)$$
3	2	adantl	$$⊢\left(X\in A\wedge x=X\right)\to \left(X=x\leftrightarrow X=X\right)$$
4		eqidd	$$⊢X\in A\to X=X$$
5	1 3 4	rspcedvd	$$⊢X\in A\to \exists x\in AX=x$$
6		eleq1a	$$⊢x\in A\to \left(X=x\to X\in A\right)$$
7	6	rexlimiv	$$⊢\exists x\in AX=x\to X\in A$$
8	5 7	impbii	$$⊢X\in A\leftrightarrow \exists x\in AX=x$$