Theorem risset

Description: Two ways to say " A belongs to B ". (Contributed by NM, 22-Nov-1994)

	Ref	Expression
Assertion	risset	$$⊢A\in B\leftrightarrow \exists x\in Bx=A$$

Proof

Step	Hyp	Ref	Expression
1		exancom	$$⊢\exists x\left(x\in B\wedge x=A\right)\leftrightarrow \exists x\left(x=A\wedge x\in B\right)$$
2		df-rex	$$⊢\exists x\in Bx=A\leftrightarrow \exists x\left(x\in B\wedge x=A\right)$$
3		dfclel	$$⊢A\in B\leftrightarrow \exists x\left(x=A\wedge x\in B\right)$$
4	1 2 3	3bitr4ri	$$⊢A\in B\leftrightarrow \exists x\in Bx=A$$