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 ( ∃! 𝑥 𝑥 ∈ 𝐴 ↔ ∃! 𝑥 ∈ 𝐴 ⊤ )

Proof

Step Hyp Ref Expression
1 rextru ⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ⊤ )
2 rmotru ⊢ ( ∃* 𝑥 𝑥 ∈ 𝐴 ↔ ∃* 𝑥 ∈ 𝐴 ⊤ )
3 1 2 anbi12i ⊢ ( ( ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∃* 𝑥 𝑥 ∈ 𝐴 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ⊤ ∧ ∃* 𝑥 ∈ 𝐴 ⊤ ) )
4 df-eu ⊢ ( ∃! 𝑥 𝑥 ∈ 𝐴 ↔ ( ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∃* 𝑥 𝑥 ∈ 𝐴 ) )
5 reu5 ⊢ ( ∃! 𝑥 ∈ 𝐴 ⊤ ↔ ( ∃ 𝑥 ∈ 𝐴 ⊤ ∧ ∃* 𝑥 ∈ 𝐴 ⊤ ) )
6 3 4 5 3bitr4i ⊢ ( ∃! 𝑥 𝑥 ∈ 𝐴 ↔ ∃! 𝑥 ∈ 𝐴 ⊤ )