Metamath Proof Explorer

Theorem reuan

Description: Introduction of a conjunct into restricted unique existential quantifier, analogous to euan . (Contributed by Alexander van der Vekens, 2-Jul-2017)

Ref Expression
Hypothesis rmoanim.1 ⊢ Ⅎ x φ
Assertion reuan ⊢ ∃! x ∈ A φ ∧ ψ ↔ φ ∧ ∃! x ∈ A ψ

Proof

Step Hyp Ref Expression
1 rmoanim.1 ⊢ Ⅎ x φ
2 simpl ⊢ φ ∧ ψ → φ
3 2 a1i ⊢ x ∈ A → φ ∧ ψ → φ
4 1 3 rexlimi ⊢ ∃ x ∈ A φ ∧ ψ → φ
5 4 adantr ⊢ ∃ x ∈ A φ ∧ ψ ∧ ∃* x ∈ A φ ∧ ψ → φ
6 simpr ⊢ φ ∧ ψ → ψ
7 6 reximi ⊢ ∃ x ∈ A φ ∧ ψ → ∃ x ∈ A ψ
8 7 adantr ⊢ ∃ x ∈ A φ ∧ ψ ∧ ∃* x ∈ A φ ∧ ψ → ∃ x ∈ A ψ
9 nfre1 ⊢ Ⅎ x ∃ x ∈ A φ ∧ ψ
10 4 adantr ⊢ ∃ x ∈ A φ ∧ ψ ∧ x ∈ A → φ
11 10 a1d ⊢ ∃ x ∈ A φ ∧ ψ ∧ x ∈ A → ψ → φ
12 11 ancrd ⊢ ∃ x ∈ A φ ∧ ψ ∧ x ∈ A → ψ → φ ∧ ψ
13 6 12 impbid2 ⊢ ∃ x ∈ A φ ∧ ψ ∧ x ∈ A → φ ∧ ψ ↔ ψ
14 9 13 rmobida ⊢ ∃ x ∈ A φ ∧ ψ → ∃* x ∈ A φ ∧ ψ ↔ ∃* x ∈ A ψ
15 14 biimpa ⊢ ∃ x ∈ A φ ∧ ψ ∧ ∃* x ∈ A φ ∧ ψ → ∃* x ∈ A ψ
16 5 8 15 jca32 ⊢ ∃ x ∈ A φ ∧ ψ ∧ ∃* x ∈ A φ ∧ ψ → φ ∧ ∃ x ∈ A ψ ∧ ∃* x ∈ A ψ
17 reu5 ⊢ ∃! x ∈ A φ ∧ ψ ↔ ∃ x ∈ A φ ∧ ψ ∧ ∃* x ∈ A φ ∧ ψ
18 reu5 ⊢ ∃! x ∈ A ψ ↔ ∃ x ∈ A ψ ∧ ∃* x ∈ A ψ
19 18 anbi2i ⊢ φ ∧ ∃! x ∈ A ψ ↔ φ ∧ ∃ x ∈ A ψ ∧ ∃* x ∈ A ψ
20 16 17 19 3imtr4i ⊢ ∃! x ∈ A φ ∧ ψ → φ ∧ ∃! x ∈ A ψ
21 ibar ⊢ φ → ψ ↔ φ ∧ ψ
22 21 adantr ⊢ φ ∧ x ∈ A → ψ ↔ φ ∧ ψ
23 1 22 reubida ⊢ φ → ∃! x ∈ A ψ ↔ ∃! x ∈ A φ ∧ ψ
24 23 biimpa ⊢ φ ∧ ∃! x ∈ A ψ → ∃! x ∈ A φ ∧ ψ
25 20 24 impbii ⊢ ∃! x ∈ A φ ∧ ψ ↔ φ ∧ ∃! x ∈ A ψ