# 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 ${⊢}\left(\left({A}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\right)\wedge \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)\to \left(\iota {x}\in {A}|{\phi }\right)=\left(\iota {x}\in {B}|{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 reuss2 ${⊢}\left(\left({A}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\right)\wedge \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)\to \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
2 simplr ${⊢}\left(\left({A}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\right)\wedge \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
3 riotasbc
4 riotacl ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\iota {x}\in {A}|{\phi }\right)\in {A}$
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 ${⊢}\left(\left({A}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\right)\wedge \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)\to \left(\iota {x}\in {A}|{\phi }\right)\in {A}$
12 ssel ${⊢}{A}\subseteq {B}\to \left(\left(\iota {x}\in {A}|{\phi }\right)\in {A}\to \left(\iota {x}\in {A}|{\phi }\right)\in {B}\right)$
13 12 ad2antrr ${⊢}\left(\left({A}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\right)\wedge \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)\to \left(\left(\iota {x}\in {A}|{\phi }\right)\in {A}\to \left(\iota {x}\in {A}|{\phi }\right)\in {B}\right)$
14 11 13 mpd ${⊢}\left(\left({A}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\right)\wedge \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)\to \left(\iota {x}\in {A}|{\phi }\right)\in {B}$
15 simprr ${⊢}\left(\left({A}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\right)\wedge \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)\to \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$
16 nfriota1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left(\iota {x}\in {A}|{\phi }\right)$
17 16 nfsbc1
18 sbceq1a
19 16 17 18 riota2f
20 14 15 19 syl2anc
21 10 20 mpbid ${⊢}\left(\left({A}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\right)\wedge \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)\to \left(\iota {x}\in {B}|{\psi }\right)=\left(\iota {x}\in {A}|{\phi }\right)$
22 21 eqcomd ${⊢}\left(\left({A}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\right)\wedge \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)\to \left(\iota {x}\in {A}|{\phi }\right)=\left(\iota {x}\in {B}|{\psi }\right)$