Metamath Proof Explorer

Theorem enpr1g

Description: { A , A } has only one element. (Contributed by FL, 15-Feb-2010)

Ref Expression
Assertion enpr1g 
|- ( A e. V -> { A , A } ~~ 1o )

Proof

Step Hyp Ref Expression
1 dfsn2 
 |-  { A } = { A , A }
2 ensn1g 
 |-  ( A e. V -> { A } ~~ 1o )
3 1 2 eqbrtrrid 
 |-  ( A e. V -> { A , A } ~~ 1o )