Metamath Proof Explorer

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 ⊢ ∃! x φ ∧ ψ ↔ φ ∧ ∃! x ψ

Proof

Step Hyp Ref Expression
1 euex ⊢ ∃! x φ ∧ ψ → ∃ x φ ∧ ψ
2 simpl ⊢ φ ∧ ψ → φ
3 2 exlimiv ⊢ ∃ x φ ∧ ψ → φ
4 1 3 syl ⊢ ∃! x φ ∧ ψ → φ
5 ibar ⊢ φ → ψ ↔ φ ∧ ψ
6 5 eubidv ⊢ φ → ∃! x ψ ↔ ∃! x φ ∧ ψ
7 6 biimprcd ⊢ ∃! x φ ∧ ψ → φ → ∃! x ψ
8 4 7 jcai ⊢ ∃! x φ ∧ ψ → φ ∧ ∃! x ψ
9 6 biimpa ⊢ φ ∧ ∃! x ψ → ∃! x φ ∧ ψ
10 8 9 impbii ⊢ ∃! x φ ∧ ψ ↔ φ ∧ ∃! x ψ