This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem riotass

Description: Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion riotass ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜑 ) → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ( ℩ 𝑥 ∈ 𝐵 𝜑 ) )

Proof

Step Hyp Ref Expression
1 reuss ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜑 ) → ∃! 𝑥 ∈ 𝐴 𝜑 )
2 riotasbc ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜑 )
3 1 2 syl ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜑 ) → [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜑 )
4 simp1 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜑 ) → 𝐴 ⊆ 𝐵 )
5 riotacl ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 )
6 1 5 syl ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜑 ) → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 )
7 4 6 sseldd ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜑 ) → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐵 )
8 simp3 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜑 ) → ∃! 𝑥 ∈ 𝐵 𝜑 )
9 nfriota1 ⊢ Ⅎ 𝑥 ( ℩ 𝑥 ∈ 𝐴 𝜑 )
10 9 nfsbc1 ⊢ Ⅎ 𝑥 [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜑
11 sbceq1a ⊢ ( 𝑥 = ( ℩ 𝑥 ∈ 𝐴 𝜑 ) → ( 𝜑 ↔ [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜑 ) )
12 9 10 11 riota2f ⊢ ( ( ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜑 ) → ( [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜑 ↔ ( ℩ 𝑥 ∈ 𝐵 𝜑 ) = ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ) )
13 7 8 12 syl2anc ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜑 ) → ( [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜑 ↔ ( ℩ 𝑥 ∈ 𝐵 𝜑 ) = ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ) )
14 3 13 mpbid ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜑 ) → ( ℩ 𝑥 ∈ 𝐵 𝜑 ) = ( ℩ 𝑥 ∈ 𝐴 𝜑 ) )
15 14 eqcomd ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜑 ) → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ( ℩ 𝑥 ∈ 𝐵 𝜑 ) )