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	⊢ ( ∃! 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∃! 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		euex	⊢ ( ∃! 𝑥 ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) )
2		simpl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 )
3	2	exlimiv	⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → 𝜑 )
4	1 3	syl	⊢ ( ∃! 𝑥 ( 𝜑 ∧ 𝜓 ) → 𝜑 )
5		ibar	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜑 ∧ 𝜓 ) ) )
6	5	eubidv	⊢ ( 𝜑 → ( ∃! 𝑥 𝜓 ↔ ∃! 𝑥 ( 𝜑 ∧ 𝜓 ) ) )
7	6	biimprcd	⊢ ( ∃! 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝜑 → ∃! 𝑥 𝜓 ) )
8	4 7	jcai	⊢ ( ∃! 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ∧ ∃! 𝑥 𝜓 ) )
9	6	biimpa	⊢ ( ( 𝜑 ∧ ∃! 𝑥 𝜓 ) → ∃! 𝑥 ( 𝜑 ∧ 𝜓 ) )
10	8 9	impbii	⊢ ( ∃! 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∃! 𝑥 𝜓 ) )