Metamath Proof Explorer


Theorem reutru

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

Ref Expression
Assertion reutru ( ∃! 𝑥 𝑥𝐴 ↔ ∃! 𝑥𝐴 ⊤ )

Proof

Step Hyp Ref Expression
1 tru
2 1 biantru ( 𝑥𝐴 ↔ ( 𝑥𝐴 ∧ ⊤ ) )
3 2 eubii ( ∃! 𝑥 𝑥𝐴 ↔ ∃! 𝑥 ( 𝑥𝐴 ∧ ⊤ ) )
4 df-reu ( ∃! 𝑥𝐴 ⊤ ↔ ∃! 𝑥 ( 𝑥𝐴 ∧ ⊤ ) )
5 3 4 bitr4i ( ∃! 𝑥 𝑥𝐴 ↔ ∃! 𝑥𝐴 ⊤ )