Metamath Proof Explorer

Theorem moriotass

Description: Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006) (Revised by NM, 16-Jun-2017)

Ref Expression
Assertion moriotass ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃* x ∈ B φ → ι x ∈ A | φ = ι x ∈ B | φ

Proof

Step Hyp Ref Expression
1 ssrexv ⊢ A ⊆ B → ∃ x ∈ A φ → ∃ x ∈ B φ
2 1 imp ⊢ A ⊆ B ∧ ∃ x ∈ A φ → ∃ x ∈ B φ
3 2 3adant3 ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃* x ∈ B φ → ∃ x ∈ B φ
4 simp3 ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃* x ∈ B φ → ∃* x ∈ B φ
5 reu5 ⊢ ∃! x ∈ B φ ↔ ∃ x ∈ B φ ∧ ∃* x ∈ B φ
6 3 4 5 sylanbrc ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃* x ∈ B φ → ∃! x ∈ B φ
7 riotass ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ → ι x ∈ A | φ = ι x ∈ B | φ
8 6 7 syld3an3 ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃* x ∈ B φ → ι x ∈ A | φ = ι x ∈ B | φ