Metamath Proof Explorer

Theorem rmotru

Description: Two ways of expressing "at most one" element. (Contributed by Zhi Wang, 19-Sep-2024) (Proof shortened by BJ, 23-Sep-2024)

Ref Expression
Assertion rmotru 
|- ( 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 mobii 
 |-  ( E* x x e. A <-> E* x ( x e. A /\ T. ) )
4 df-rmo 
 |-  ( 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. )