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. )