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 ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐵 𝜑 ) → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ( ℩ 𝑥 ∈ 𝐵 𝜑 ) )

Proof

Step Hyp Ref Expression
1 ssrexv ⊢ ( 𝐴 ⊆ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐵 𝜑 ) )
2 1 imp ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) → ∃ 𝑥 ∈ 𝐵 𝜑 )
3 2 3adant3 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐵 𝜑 ) → ∃ 𝑥 ∈ 𝐵 𝜑 )
4 simp3 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐵 𝜑 ) → ∃* 𝑥 ∈ 𝐵 𝜑 )
5 reu5 ⊢ ( ∃! 𝑥 ∈ 𝐵 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐵 𝜑 ∧ ∃* 𝑥 ∈ 𝐵 𝜑 ) )
6 3 4 5 sylanbrc ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐵 𝜑 ) → ∃! 𝑥 ∈ 𝐵 𝜑 )
7 riotass ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜑 ) → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ( ℩ 𝑥 ∈ 𝐵 𝜑 ) )
8 6 7 syld3an3 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐵 𝜑 ) → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ( ℩ 𝑥 ∈ 𝐵 𝜑 ) )