Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 moanim.1 ⊢ Ⅎ x φ
2 euex ⊢ ∃! x φ ∧ ψ → ∃ x φ ∧ ψ
3 simpl ⊢ φ ∧ ψ → φ
4 1 3 exlimi ⊢ ∃ x φ ∧ ψ → φ
5 2 4 syl ⊢ ∃! x φ ∧ ψ → φ
6 ibar ⊢ φ → ψ ↔ φ ∧ ψ
7 1 6 eubid ⊢ φ → ∃! x ψ ↔ ∃! x φ ∧ ψ
8 7 biimprcd ⊢ ∃! x φ ∧ ψ → φ → ∃! x ψ
9 5 8 jcai ⊢ ∃! x φ ∧ ψ → φ ∧ ∃! x ψ
10 7 biimpa ⊢ φ ∧ ∃! x ψ → ∃! x φ ∧ ψ
11 9 10 impbii ⊢ ∃! x φ ∧ ψ ↔ φ ∧ ∃! x ψ