Theorem eubiiOLD

Description: Obsolete version of eubii as of 27-Sep-2023. (Contributed by NM, 9-Jul-1994) (Revised by Mario Carneiro, 6-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	eubii.1	$$⊢\phi \leftrightarrow \psi$$
Assertion	eubiiOLD	$$⊢\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$$