Theorem 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	$$⊢\phi \leftrightarrow \psi$$
Assertion	eubii	$$⊢\exists !x\phi \leftrightarrow \exists !x\psi$$

Proof

Step	Hyp	Ref	Expression
1		eubii.1	$$⊢\phi \leftrightarrow \psi$$
2	1	exbii	$$⊢\exists x\phi \leftrightarrow \exists x\psi$$
3	1	mobii	$$⊢{\exists }^{*}x\phi \leftrightarrow {\exists }^{*}x\psi$$
4	2 3	anbi12i	$$⊢\left(\exists x\phi \wedge {\exists }^{*}x\phi \right)\leftrightarrow \left(\exists x\psi \wedge {\exists }^{*}x\psi \right)$$
5		df-eu	$$⊢\exists !x\phi \leftrightarrow \left(\exists x\phi \wedge {\exists }^{*}x\phi \right)$$
6		df-eu	$$⊢\exists !x\psi \leftrightarrow \left(\exists x\psi \wedge {\exists }^{*}x\psi \right)$$
7	4 5 6	3bitr4i	$$⊢\exists !x\phi \leftrightarrow \exists !x\psi$$