# Metamath Proof Explorer

## Theorem reuxfrdf

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Cf. reuxfrd (Contributed by Thierry Arnoux, 7-Apr-2017) (Revised by Thierry Arnoux, 8-Oct-2017) (Revised by Thierry Arnoux, 30-Mar-2018)

Ref Expression
Hypotheses reuxfrdf.0 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{B}$
reuxfrdf.1 ${⊢}\left({\phi }\wedge {y}\in {C}\right)\to {A}\in {B}$
reuxfrdf.2 ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {\exists }^{*}{y}\in {C}{x}={A}$
Assertion reuxfrdf ${⊢}{\phi }\to \left(\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)↔\exists !{y}\in {C}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 reuxfrdf.0 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{B}$
2 reuxfrdf.1 ${⊢}\left({\phi }\wedge {y}\in {C}\right)\to {A}\in {B}$
3 reuxfrdf.2 ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {\exists }^{*}{y}\in {C}{x}={A}$
4 rmoan ${⊢}{\exists }^{*}{y}\in {C}{x}={A}\to {\exists }^{*}{y}\in {C}\left({\psi }\wedge {x}={A}\right)$
5 3 4 syl ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {\exists }^{*}{y}\in {C}\left({\psi }\wedge {x}={A}\right)$
6 ancom ${⊢}\left({\psi }\wedge {x}={A}\right)↔\left({x}={A}\wedge {\psi }\right)$
7 6 rmobii ${⊢}{\exists }^{*}{y}\in {C}\left({\psi }\wedge {x}={A}\right)↔{\exists }^{*}{y}\in {C}\left({x}={A}\wedge {\psi }\right)$
8 5 7 sylib ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {\exists }^{*}{y}\in {C}\left({x}={A}\wedge {\psi }\right)$
9 8 ralrimiva ${⊢}{\phi }\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\in {C}\left({x}={A}\wedge {\psi }\right)$
10 df-rmo ${⊢}{\exists }^{*}{y}\in {C}\left({x}={A}\wedge {\psi }\right)↔{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)$
11 10 ralbii ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\in {C}\left({x}={A}\wedge {\psi }\right)↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)$
12 df-ral ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
13 1 nfcri ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}\in {B}$
14 13 moanim ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)↔\left({x}\in {B}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
15 14 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
16 12 15 bitr4i ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
17 2euswapv ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)\to \left(\exists !{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)\to \exists !{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)\right)$
18 df-reu ${⊢}\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)↔\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)$
19 13 r19.41 ${⊢}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left(\left({x}={A}\wedge {\psi }\right)\wedge {x}\in {B}\right)↔\left(\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\wedge {x}\in {B}\right)$
20 ancom ${⊢}\left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)↔\left(\left({x}={A}\wedge {\psi }\right)\wedge {x}\in {B}\right)$
21 20 rexbii ${⊢}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)↔\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left(\left({x}={A}\wedge {\psi }\right)\wedge {x}\in {B}\right)$
22 ancom ${⊢}\left({x}\in {B}\wedge \exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)↔\left(\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\wedge {x}\in {B}\right)$
23 19 21 22 3bitr4i ${⊢}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)↔\left({x}\in {B}\wedge \exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)$
24 df-rex ${⊢}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
25 23 24 bitr3i ${⊢}\left({x}\in {B}\wedge \exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
26 an12 ${⊢}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)↔\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
27 26 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
28 25 27 bitri ${⊢}\left({x}\in {B}\wedge \exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
29 28 eubii ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)↔\exists !{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
30 18 29 bitri ${⊢}\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)↔\exists !{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
31 df-reu ${⊢}\exists !{y}\in {C}\phantom{\rule{.4em}{0ex}}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)↔\exists !{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)$
32 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {C}$
33 32 r19.41 ${⊢}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}={A}\wedge {\psi }\right)\wedge {y}\in {C}\right)↔\left(\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\wedge {y}\in {C}\right)$
34 ancom ${⊢}\left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)↔\left(\left({x}={A}\wedge {\psi }\right)\wedge {y}\in {C}\right)$
35 34 rexbii ${⊢}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)↔\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}={A}\wedge {\psi }\right)\wedge {y}\in {C}\right)$
36 ancom ${⊢}\left({y}\in {C}\wedge \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)↔\left(\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\wedge {y}\in {C}\right)$
37 33 35 36 3bitr4i ${⊢}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)↔\left({y}\in {C}\wedge \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)$
38 df-rex ${⊢}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
39 37 38 bitr3i ${⊢}\left({y}\in {C}\wedge \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
40 39 eubii ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)↔\exists !{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
41 31 40 bitri ${⊢}\exists !{y}\in {C}\phantom{\rule{.4em}{0ex}}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)↔\exists !{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
42 17 30 41 3imtr4g ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)\to \left(\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\to \exists !{y}\in {C}\phantom{\rule{.4em}{0ex}}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)$
43 16 42 sylbi ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\to \left(\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\to \exists !{y}\in {C}\phantom{\rule{.4em}{0ex}}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)$
44 11 43 sylbi ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\in {C}\left({x}={A}\wedge {\psi }\right)\to \left(\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\to \exists !{y}\in {C}\phantom{\rule{.4em}{0ex}}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)$
45 9 44 syl ${⊢}{\phi }\to \left(\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\to \exists !{y}\in {C}\phantom{\rule{.4em}{0ex}}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)$
46 df-ral ${⊢}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
47 moanimv ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)↔\left({y}\in {C}\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
48 47 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
49 46 48 bitr4i ${⊢}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
50 2euswapv ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)\to \left(\exists !{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)\to \exists !{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)\right)$
51 r19.42v ${⊢}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)↔\left({y}\in {C}\wedge \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)$
52 51 38 bitr3i ${⊢}\left({y}\in {C}\wedge \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
53 an12 ${⊢}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)↔\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
54 53 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({y}\in {C}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
55 52 54 bitri ${⊢}\left({y}\in {C}\wedge \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
56 55 eubii ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)↔\exists !{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
57 31 56 bitri ${⊢}\exists !{y}\in {C}\phantom{\rule{.4em}{0ex}}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)↔\exists !{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
58 25 eubii ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)↔\exists !{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
59 18 58 bitri ${⊢}\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)↔\exists !{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)$
60 50 57 59 3imtr4g ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\wedge \left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\right)\to \left(\exists !{y}\in {C}\phantom{\rule{.4em}{0ex}}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\to \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)$
61 49 60 sylbi ${⊢}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)\to \left(\exists !{y}\in {C}\phantom{\rule{.4em}{0ex}}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\to \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)$
62 moeq ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{x}={A}$
63 62 moani ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {B}\wedge {\psi }\right)\wedge {x}={A}\right)$
64 ancom ${⊢}\left(\left({x}\in {B}\wedge {\psi }\right)\wedge {x}={A}\right)↔\left({x}={A}\wedge \left({x}\in {B}\wedge {\psi }\right)\right)$
65 an12 ${⊢}\left({x}={A}\wedge \left({x}\in {B}\wedge {\psi }\right)\right)↔\left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)$
66 64 65 bitri ${⊢}\left(\left({x}\in {B}\wedge {\psi }\right)\wedge {x}={A}\right)↔\left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)$
67 66 mobii ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {B}\wedge {\psi }\right)\wedge {x}={A}\right)↔{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)$
68 63 67 mpbi ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)$
69 68 a1i ${⊢}{y}\in {C}\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge \left({x}={A}\wedge {\psi }\right)\right)$
70 61 69 mprg ${⊢}\exists !{y}\in {C}\phantom{\rule{.4em}{0ex}}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\to \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)$
71 45 70 impbid1 ${⊢}{\phi }\to \left(\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)↔\exists !{y}\in {C}\phantom{\rule{.4em}{0ex}}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)\right)$
72 biidd ${⊢}{x}={A}\to \left({\psi }↔{\psi }\right)$
73 72 ceqsrexv ${⊢}{A}\in {B}\to \left(\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)↔{\psi }\right)$
74 2 73 syl ${⊢}\left({\phi }\wedge {y}\in {C}\right)\to \left(\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)↔{\psi }\right)$
75 74 reubidva ${⊢}{\phi }\to \left(\exists !{y}\in {C}\phantom{\rule{.4em}{0ex}}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)↔\exists !{y}\in {C}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
76 71 75 bitrd ${⊢}{\phi }\to \left(\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\psi }\right)↔\exists !{y}\in {C}\phantom{\rule{.4em}{0ex}}{\psi }\right)$