Metamath Proof Explorer


Theorem reutru

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

Ref Expression
Assertion reutru
|- ( E! x x e. A <-> E! x e. A T. )

Proof

Step Hyp Ref Expression
1 tru
 |-  T.
2 1 biantru
 |-  ( x e. A <-> ( x e. A /\ T. ) )
3 2 eubii
 |-  ( E! x x e. A <-> E! x ( x e. A /\ T. ) )
4 df-reu
 |-  ( E! x e. A T. <-> E! x ( x e. A /\ T. ) )
5 3 4 bitr4i
 |-  ( E! x x e. A <-> E! x e. A T. )