This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Uniqueness and unique existence Unique existence: the unique existential quantifier eubii
Description: Introduce unique existential quantifier to both sides of an equivalence.
(Contributed by NM , 9-Jul-1994) (Revised by Mario Carneiro , 6-Oct-2016) Avoid ax-5 . (Revised by Wolf Lammen , 27-Sep-2023)
Ref
Expression
Hypothesis
eubii.1 ⊢ ( 𝜑 ↔ 𝜓 )
Assertion
eubii ⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑥 𝜓 )
Proof
Step
Hyp
Ref
Expression
1
eubii.1 ⊢ ( 𝜑 ↔ 𝜓 )
2
1
exbii ⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 𝜓 )
3
1
mobii ⊢ ( ∃* 𝑥 𝜑 ↔ ∃* 𝑥 𝜓 )
4
2 3
anbi12i ⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) ↔ ( ∃ 𝑥 𝜓 ∧ ∃* 𝑥 𝜓 ) )
5
df-eu ⊢ ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) )
6
df-eu ⊢ ( ∃! 𝑥 𝜓 ↔ ( ∃ 𝑥 𝜓 ∧ ∃* 𝑥 𝜓 ) )
7
4 5 6
3bitr4i ⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑥 𝜓 )