Metamath Proof Explorer


Theorem reutru

Description: Two ways of expressing "exactly one" element. (Contributed by Zhi Wang, 23-Sep-2024)

Ref Expression
Assertion reutru ∃!xxA∃!xA

Proof

Step Hyp Ref Expression
1 tru
2 1 biantru xAxA
3 2 eubii ∃!xxA∃!xxA
4 df-reu ∃!xA∃!xxA
5 3 4 bitr4i ∃!xxA∃!xA