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	|- F/ x ph
Assertion	euan	|- ( E! x ( ph /\ ps ) <-> ( ph /\ E! x ps ) )

Proof

Step	Hyp	Ref	Expression
1		moanim.1	|- F/ x ph
2		euex	|- ( E! x ( ph /\ ps ) -> E. x ( ph /\ ps ) )
3		simpl	|- ( ( ph /\ ps ) -> ph )
4	1 3	exlimi	|- ( E. x ( ph /\ ps ) -> ph )
5	2 4	syl	|- ( E! x ( ph /\ ps ) -> ph )
6		ibar	|- ( ph -> ( ps <-> ( ph /\ ps ) ) )
7	1 6	eubid	|- ( ph -> ( E! x ps <-> E! x ( ph /\ ps ) ) )
8	7	biimprcd	|- ( E! x ( ph /\ ps ) -> ( ph -> E! x ps ) )
9	5 8	jcai	|- ( E! x ( ph /\ ps ) -> ( ph /\ E! x ps ) )
10	7	biimpa	|- ( ( ph /\ E! x ps ) -> E! x ( ph /\ ps ) )
11	9 10	impbii	|- ( E! x ( ph /\ ps ) <-> ( ph /\ E! x ps ) )