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 e. _V
Assertion intsn
|- |^| { A } = A

Proof

Step Hyp Ref Expression
1 intsn.1
 |-  A e. _V
2 intsng
 |-  ( A e. _V -> |^| { A } = A )
3 1 2 ax-mp
 |-  |^| { A } = A