Metamath Proof Explorer

Theorem rextru

Description: Two ways of expressing that a class has at least one element. (Contributed by Zhi Wang, 23-Sep-2024)

Ref Expression
Assertion rextru 
|- ( 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 exbii 
 |-  ( E. x x e. A <-> E. x ( x e. A /\ T. ) )
4 df-rex 
 |-  ( 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. )