Description: Idempotent law for intersection of classes. Theorem 15 of Suppes p. 26. (Contributed by NM, 5-Aug-1993)
Ref | Expression | ||
---|---|---|---|
Assertion | inidm | ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anidm | ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ↔ 𝑥 ∈ 𝐴 ) | |
2 | 1 | ineqri | ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴 |