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