# Metamath Proof Explorer

## Theorem riota2df

Description: A deduction version of riota2f . (Contributed by NM, 17-Feb-2013) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses riota2df.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
riota2df.2 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
riota2df.3 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
riota2df.4 ${⊢}{\phi }\to {B}\in {A}$
riota2df.5 ${⊢}\left({\phi }\wedge {x}={B}\right)\to \left({\psi }↔{\chi }\right)$
Assertion riota2df ${⊢}\left({\phi }\wedge \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \left({\chi }↔\left(\iota {x}\in {A}|{\psi }\right)={B}\right)$

### Proof

Step Hyp Ref Expression
1 riota2df.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 riota2df.2 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
3 riota2df.3 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
4 riota2df.4 ${⊢}{\phi }\to {B}\in {A}$
5 riota2df.5 ${⊢}\left({\phi }\wedge {x}={B}\right)\to \left({\psi }↔{\chi }\right)$
6 4 adantr ${⊢}\left({\phi }\wedge \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to {B}\in {A}$
7 simpr ${⊢}\left({\phi }\wedge \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }$
8 df-reu ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\psi }\right)$
9 7 8 sylib ${⊢}\left({\phi }\wedge \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\psi }\right)$
10 simpr ${⊢}\left(\left({\phi }\wedge \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\wedge {x}={B}\right)\to {x}={B}$
11 6 adantr ${⊢}\left(\left({\phi }\wedge \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\wedge {x}={B}\right)\to {B}\in {A}$
12 10 11 eqeltrd ${⊢}\left(\left({\phi }\wedge \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\wedge {x}={B}\right)\to {x}\in {A}$
13 12 biantrurd ${⊢}\left(\left({\phi }\wedge \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\wedge {x}={B}\right)\to \left({\psi }↔\left({x}\in {A}\wedge {\psi }\right)\right)$
14 5 adantlr ${⊢}\left(\left({\phi }\wedge \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\wedge {x}={B}\right)\to \left({\psi }↔{\chi }\right)$
15 13 14 bitr3d ${⊢}\left(\left({\phi }\wedge \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\wedge {x}={B}\right)\to \left(\left({x}\in {A}\wedge {\psi }\right)↔{\chi }\right)$
16 nfreu1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }$
17 1 16 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
18 3 adantr ${⊢}\left({\phi }\wedge \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
19 2 adantr ${⊢}\left({\phi }\wedge \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
20 6 9 15 17 18 19 iota2df ${⊢}\left({\phi }\wedge \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \left({\chi }↔\left(\iota {x}|\left({x}\in {A}\wedge {\psi }\right)\right)={B}\right)$
21 df-riota ${⊢}\left(\iota {x}\in {A}|{\psi }\right)=\left(\iota {x}|\left({x}\in {A}\wedge {\psi }\right)\right)$
22 21 eqeq1i ${⊢}\left(\iota {x}\in {A}|{\psi }\right)={B}↔\left(\iota {x}|\left({x}\in {A}\wedge {\psi }\right)\right)={B}$
23 20 22 syl6bbr ${⊢}\left({\phi }\wedge \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \left({\chi }↔\left(\iota {x}\in {A}|{\psi }\right)={B}\right)$