Metamath Proof Explorer


Theorem enpr1g

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

Ref Expression
Assertion enpr1g AVAA1𝑜

Proof

Step Hyp Ref Expression
1 dfsn2 A=AA
2 ensn1g AVA1𝑜
3 1 2 eqbrtrrid AVAA1𝑜