Theorem riotaeqimp

Description: If two restricted iota descriptors for an equality are equal, then the terms of the equality are equal. (Contributed by AV, 6-Dec-2020)

	Ref	Expression
Hypotheses	riotaeqimp.i	$$⊢I=\left(\iota a\in V|X=A\right)$$
	riotaeqimp.j	$$⊢J=\left(\iota a\in V|Y=A\right)$$
	riotaeqimp.x	$$⊢\phi \to \exists !a\in VX=A$$
	riotaeqimp.y	$$⊢\phi \to \exists !a\in VY=A$$
Assertion	riotaeqimp	$$⊢\left(\phi \wedge I=J\right)\to X=Y$$

Proof

Step	Hyp	Ref	Expression
1		riotaeqimp.i	$$⊢I=\left(\iota a\in V|X=A\right)$$
2		riotaeqimp.j	$$⊢J=\left(\iota a\in V|Y=A\right)$$
3		riotaeqimp.x	$$⊢\phi \to \exists !a\in VX=A$$
4		riotaeqimp.y	$$⊢\phi \to \exists !a\in VY=A$$
5	2	eqcomi	$$⊢\left(\iota a\in V|Y=A\right)=J$$
6	5	eqeq2i	$$⊢I=\left(\iota a\in V|Y=A\right)\leftrightarrow I=J$$
7	6	a1i	$$⊢\phi \to \left(I=\left(\iota a\in V|Y=A\right)\leftrightarrow I=J\right)$$
8	7	bicomd	$$⊢\phi \to \left(I=J\leftrightarrow I=\left(\iota a\in V|Y=A\right)\right)$$
9	8	biimpa	$$⊢\left(\phi \wedge I=J\right)\to I=\left(\iota a\in V|Y=A\right)$$
10	1	eqeq1i	$$⊢I=J\leftrightarrow \left(\iota a\in V|X=A\right)=J$$
11		riotacl	$$⊢\exists !a\in VY=A\to \left(\iota a\in V|Y=A\right)\in V$$
12	4 11	syl	$$⊢\phi \to \left(\iota a\in V|Y=A\right)\in V$$
13	2 12	eqeltrid	$$⊢\phi \to J\in V$$
14		nfv	$$⊢ℲaJ\in V$$
15		nfcvd	$$⊢J\in V\to \underset{\_}{Ⅎ}aJ$$
16		nfcvd	$$⊢J\in V\to \underset{\_}{Ⅎ}aX$$
17	15	nfcsb1d	$$⊢J\in V\to \underset{\_}{Ⅎ}a⦋J/a⦌A$$
18	16 17	nfeqd	$$⊢J\in V\to ℲaX=⦋J/a⦌A$$
19		id	$$⊢J\in V\to J\in V$$
20		csbeq1a	$$⊢a=J\to A=⦋J/a⦌A$$
21	20	eqeq2d	$$⊢a=J\to \left(X=A\leftrightarrow X=⦋J/a⦌A\right)$$
22	21	adantl	$$⊢\left(J\in V\wedge a=J\right)\to \left(X=A\leftrightarrow X=⦋J/a⦌A\right)$$
23	14 15 18 19 22	riota2df	$$⊢\left(J\in V\wedge \exists !a\in VX=A\right)\to \left(X=⦋J/a⦌A\leftrightarrow \left(\iota a\in V|X=A\right)=J\right)$$
24	23	bicomd	$$⊢\left(J\in V\wedge \exists !a\in VX=A\right)\to \left(\left(\iota a\in V|X=A\right)=J\leftrightarrow X=⦋J/a⦌A\right)$$
25	13 3 24	syl2anc	$$⊢\phi \to \left(\left(\iota a\in V|X=A\right)=J\leftrightarrow X=⦋J/a⦌A\right)$$
26	10 25	bitrid	$$⊢\phi \to \left(I=J\leftrightarrow X=⦋J/a⦌A\right)$$
27	26	biimpa	$$⊢\left(\phi \wedge I=J\right)\to X=⦋J/a⦌A$$
28		riotacl	$$⊢\exists !a\in VX=A\to \left(\iota a\in V|X=A\right)\in V$$
29	3 28	syl	$$⊢\phi \to \left(\iota a\in V|X=A\right)\in V$$
30	1 29	eqeltrid	$$⊢\phi \to I\in V$$
31		nfv	$$⊢ℲaI\in V$$
32		nfcvd	$$⊢I\in V\to \underset{\_}{Ⅎ}aI$$
33		nfcvd	$$⊢I\in V\to \underset{\_}{Ⅎ}aY$$
34	32	nfcsb1d	$$⊢I\in V\to \underset{\_}{Ⅎ}a⦋I/a⦌A$$
35	33 34	nfeqd	$$⊢I\in V\to ℲaY=⦋I/a⦌A$$
36		id	$$⊢I\in V\to I\in V$$
37		csbeq1a	$$⊢a=I\to A=⦋I/a⦌A$$
38	37	eqeq2d	$$⊢a=I\to \left(Y=A\leftrightarrow Y=⦋I/a⦌A\right)$$
39	38	adantl	$$⊢\left(I\in V\wedge a=I\right)\to \left(Y=A\leftrightarrow Y=⦋I/a⦌A\right)$$
40	31 32 35 36 39	riota2df	$$⊢\left(I\in V\wedge \exists !a\in VY=A\right)\to \left(Y=⦋I/a⦌A\leftrightarrow \left(\iota a\in V|Y=A\right)=I\right)$$
41	30 4 40	syl2anc	$$⊢\phi \to \left(Y=⦋I/a⦌A\leftrightarrow \left(\iota a\in V|Y=A\right)=I\right)$$
42		eqcom	$$⊢\left(\iota a\in V|Y=A\right)=I\leftrightarrow I=\left(\iota a\in V|Y=A\right)$$
43	41 42	bitrdi	$$⊢\phi \to \left(Y=⦋I/a⦌A\leftrightarrow I=\left(\iota a\in V|Y=A\right)\right)$$
44	43	adantr	$$⊢\left(\phi \wedge I=J\right)\to \left(Y=⦋I/a⦌A\leftrightarrow I=\left(\iota a\in V|Y=A\right)\right)$$
45		csbeq1	$$⊢J=I\to ⦋J/a⦌A=⦋I/a⦌A$$
46	45	eqcoms	$$⊢I=J\to ⦋J/a⦌A=⦋I/a⦌A$$
47		eqeq12	$$⊢\left(X=⦋J/a⦌A\wedge Y=⦋I/a⦌A\right)\to \left(X=Y\leftrightarrow ⦋J/a⦌A=⦋I/a⦌A\right)$$
48	47	ancoms	$$⊢\left(Y=⦋I/a⦌A\wedge X=⦋J/a⦌A\right)\to \left(X=Y\leftrightarrow ⦋J/a⦌A=⦋I/a⦌A\right)$$
49	46 48	syl5ibrcom	$$⊢I=J\to \left(\left(Y=⦋I/a⦌A\wedge X=⦋J/a⦌A\right)\to X=Y\right)$$
50	49	expd	$$⊢I=J\to \left(Y=⦋I/a⦌A\to \left(X=⦋J/a⦌A\to X=Y\right)\right)$$
51	50	adantl	$$⊢\left(\phi \wedge I=J\right)\to \left(Y=⦋I/a⦌A\to \left(X=⦋J/a⦌A\to X=Y\right)\right)$$
52	44 51	sylbird	$$⊢\left(\phi \wedge I=J\right)\to \left(I=\left(\iota a\in V|Y=A\right)\to \left(X=⦋J/a⦌A\to X=Y\right)\right)$$
53	9 27 52	mp2d	$$⊢\left(\phi \wedge I=J\right)\to X=Y$$