Theorem inidm

Description: Idempotent law for intersection of classes. Theorem 15 of Suppes p. 26. (Contributed by NM, 5-Aug-1993)

	Ref	Expression
Assertion	inidm	$$⊢A\cap A=A$$

Proof

Step	Hyp	Ref	Expression
1		anidm	$$⊢\left(x\in A\wedge x\in A\right)\leftrightarrow x\in A$$
2	1	ineqri	$$⊢A\cap A=A$$