Metamath Proof Explorer

Theorem reutruALT

Description: Alternate proof for reutru . (Contributed by Zhi Wang, 23-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 rextru 
 |-  ( E. x x e. A <-> E. x e. A T. )
2 rmotru 
 |-  ( E* x x e. A <-> E* x e. A T. )
3 1 2 anbi12i 
 |-  ( ( E. x x e. A /\ E* x x e. A ) <-> ( E. x e. A T. /\ E* x e. A T. ) )
4 df-eu 
 |-  ( E! x x e. A <-> ( E. x x e. A /\ E* x x e. A ) )
5 reu5 
 |-  ( E! x e. A T. <-> ( E. x e. A T. /\ E* x e. A T. ) )
6 3 4 5 3bitr4i 
 |-  ( E! x x e. A <-> E! x e. A T. )