Metamath Proof Explorer

Theorem riotass2

Description: Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011) (Revised by NM, 22-Mar-2013)

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

Proof

Step Hyp Ref Expression
1 reuss2 ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) ∧ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) → ∃! 𝑥 ∈ 𝐴 𝜑 )
2 simplr ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) ∧ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) )
3 riotasbc ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜑 )
4 riotacl ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 )
5 rspsbc ⊢ ( ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] ( 𝜑 → 𝜓 ) ) )
6 sbcimg ⊢ ( ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 → ( [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ( [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜑 → [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜓 ) ) )
7 5 6 sylibd ⊢ ( ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ( [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜑 → [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜓 ) ) )
8 4 7 syl ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ( [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜑 → [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜓 ) ) )
9 3 8 mpid ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜓 ) )
10 1 2 9 sylc ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) ∧ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) → [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜓 )
11 1 4 syl ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) ∧ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 )
12 ssel ⊢ ( 𝐴 ⊆ 𝐵 → ( ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐵 ) )
13 12 ad2antrr ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) ∧ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) → ( ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐵 ) )
14 11 13 mpd ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) ∧ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐵 )
15 simprr ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) ∧ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) → ∃! 𝑥 ∈ 𝐵 𝜓 )
16 nfriota1 ⊢ Ⅎ 𝑥 ( ℩ 𝑥 ∈ 𝐴 𝜑 )
17 16 nfsbc1 ⊢ Ⅎ 𝑥 [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜓
18 sbceq1a ⊢ ( 𝑥 = ( ℩ 𝑥 ∈ 𝐴 𝜑 ) → ( 𝜓 ↔ [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜓 ) )
19 16 17 18 riota2f ⊢ ( ( ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) → ( [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜓 ↔ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) = ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ) )
20 14 15 19 syl2anc ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) ∧ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) → ( [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜓 ↔ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) = ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ) )
21 10 20 mpbid ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) ∧ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) → ( ℩ 𝑥 ∈ 𝐵 𝜓 ) = ( ℩ 𝑥 ∈ 𝐴 𝜑 ) )
22 21 eqcomd ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) ∧ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )