Theorem euan

Description: Introduction of a conjunct into unique existential quantifier. (Contributed by NM, 19-Feb-2005) (Proof shortened by Andrew Salmon, 9-Jul-2011) (Proof shortened by Wolf Lammen, 24-Dec-2018)

	Ref	Expression
Hypothesis	moanim.1	$$⊢Ⅎx\phi$$
Assertion	euan	$$⊢\exists !x\left(\phi \wedge \psi \right)\leftrightarrow \left(\phi \wedge \exists !x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		moanim.1	$$⊢Ⅎx\phi$$
2		euex	$$⊢\exists !x\left(\phi \wedge \psi \right)\to \exists x\left(\phi \wedge \psi \right)$$
3		simpl	$$⊢\left(\phi \wedge \psi \right)\to \phi$$
4	1 3	exlimi	$$⊢\exists x\left(\phi \wedge \psi \right)\to \phi$$
5	2 4	syl	$$⊢\exists !x\left(\phi \wedge \psi \right)\to \phi$$
6		ibar	$$⊢\phi \to \left(\psi \leftrightarrow \left(\phi \wedge \psi \right)\right)$$
7	1 6	eubid	$$⊢\phi \to \left(\exists !x\psi \leftrightarrow \exists !x\left(\phi \wedge \psi \right)\right)$$
8	7	biimprcd	$$⊢\exists !x\left(\phi \wedge \psi \right)\to \left(\phi \to \exists !x\psi \right)$$
9	5 8	jcai	$$⊢\exists !x\left(\phi \wedge \psi \right)\to \left(\phi \wedge \exists !x\psi \right)$$
10	7	biimpa	$$⊢\left(\phi \wedge \exists !x\psi \right)\to \exists !x\left(\phi \wedge \psi \right)$$
11	9 10	impbii	$$⊢\exists !x\left(\phi \wedge \psi \right)\leftrightarrow \left(\phi \wedge \exists !x\psi \right)$$