Theorem euanv

Description: Introduction of a conjunct into unique existential quantifier. (Contributed by NM, 23-Mar-1995) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2023)

	Ref	Expression
Assertion	euanv	|- ( E! x ( ph /\ ps ) <-> ( ph /\ E! x ps ) )

Proof

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