Metamath Proof Explorer


Theorem intsn

Description: The intersection of a singleton is its member. Theorem 70 of Suppes p. 41. (Contributed by NM, 29-Sep-2002)

Ref Expression
Hypothesis intsn.1 A V
Assertion intsn A = A

Proof

Step Hyp Ref Expression
1 intsn.1 A V
2 intsng A V A = A
3 1 2 ax-mp A = A