Metamath Proof Explorer


Theorem enpr1g

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

Ref Expression
Assertion enpr1g A V A A 1 𝑜

Proof

Step Hyp Ref Expression
1 dfsn2 A = A A
2 ensn1g A V A 1 𝑜
3 1 2 eqbrtrrid A V A A 1 𝑜