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)

	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		eubi	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\exists !x\phi \leftrightarrow \exists !x\psi \right)$$
3	2 1	mpg	$$⊢\exists !x\phi \leftrightarrow \exists !x\psi$$