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