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	⊢ 𝐼 = ( ℩ 𝑎 ∈ 𝑉 𝑋 = 𝐴 )
	riotaeqimp.j	⊢ 𝐽 = ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 )
	riotaeqimp.x	⊢ ( 𝜑 → ∃! 𝑎 ∈ 𝑉 𝑋 = 𝐴 )
	riotaeqimp.y	⊢ ( 𝜑 → ∃! 𝑎 ∈ 𝑉 𝑌 = 𝐴 )
Assertion	riotaeqimp	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → 𝑋 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		riotaeqimp.i	⊢ 𝐼 = ( ℩ 𝑎 ∈ 𝑉 𝑋 = 𝐴 )
2		riotaeqimp.j	⊢ 𝐽 = ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 )
3		riotaeqimp.x	⊢ ( 𝜑 → ∃! 𝑎 ∈ 𝑉 𝑋 = 𝐴 )
4		riotaeqimp.y	⊢ ( 𝜑 → ∃! 𝑎 ∈ 𝑉 𝑌 = 𝐴 )
5	2	eqcomi	⊢ ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) = 𝐽
6	5	eqeq2i	⊢ ( 𝐼 = ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) ↔ 𝐼 = 𝐽 )
7	6	a1i	⊢ ( 𝜑 → ( 𝐼 = ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) ↔ 𝐼 = 𝐽 ) )
8	7	bicomd	⊢ ( 𝜑 → ( 𝐼 = 𝐽 ↔ 𝐼 = ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) ) )
9	8	biimpa	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → 𝐼 = ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) )
10	1	eqeq1i	⊢ ( 𝐼 = 𝐽 ↔ ( ℩ 𝑎 ∈ 𝑉 𝑋 = 𝐴 ) = 𝐽 )
11		riotacl	⊢ ( ∃! 𝑎 ∈ 𝑉 𝑌 = 𝐴 → ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) ∈ 𝑉 )
12	4 11	syl	⊢ ( 𝜑 → ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) ∈ 𝑉 )
13	2 12	eqeltrid	⊢ ( 𝜑 → 𝐽 ∈ 𝑉 )
14		nfv	⊢ Ⅎ 𝑎 𝐽 ∈ 𝑉
15		nfcvd	⊢ ( 𝐽 ∈ 𝑉 → Ⅎ 𝑎 𝐽 )
16		nfcvd	⊢ ( 𝐽 ∈ 𝑉 → Ⅎ 𝑎 𝑋 )
17	15	nfcsb1d	⊢ ( 𝐽 ∈ 𝑉 → Ⅎ 𝑎 ⦋ 𝐽 / 𝑎 ⦌ 𝐴 )
18	16 17	nfeqd	⊢ ( 𝐽 ∈ 𝑉 → Ⅎ 𝑎 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 )
19		id	⊢ ( 𝐽 ∈ 𝑉 → 𝐽 ∈ 𝑉 )
20		csbeq1a	⊢ ( 𝑎 = 𝐽 → 𝐴 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 )
21	20	eqeq2d	⊢ ( 𝑎 = 𝐽 → ( 𝑋 = 𝐴 ↔ 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ) )
22	21	adantl	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝑎 = 𝐽 ) → ( 𝑋 = 𝐴 ↔ 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ) )
23	14 15 18 19 22	riota2df	⊢ ( ( 𝐽 ∈ 𝑉 ∧ ∃! 𝑎 ∈ 𝑉 𝑋 = 𝐴 ) → ( 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ↔ ( ℩ 𝑎 ∈ 𝑉 𝑋 = 𝐴 ) = 𝐽 ) )
24	23	bicomd	⊢ ( ( 𝐽 ∈ 𝑉 ∧ ∃! 𝑎 ∈ 𝑉 𝑋 = 𝐴 ) → ( ( ℩ 𝑎 ∈ 𝑉 𝑋 = 𝐴 ) = 𝐽 ↔ 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ) )
25	13 3 24	syl2anc	⊢ ( 𝜑 → ( ( ℩ 𝑎 ∈ 𝑉 𝑋 = 𝐴 ) = 𝐽 ↔ 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ) )
26	10 25	bitrid	⊢ ( 𝜑 → ( 𝐼 = 𝐽 ↔ 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ) )
27	26	biimpa	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 )
28		riotacl	⊢ ( ∃! 𝑎 ∈ 𝑉 𝑋 = 𝐴 → ( ℩ 𝑎 ∈ 𝑉 𝑋 = 𝐴 ) ∈ 𝑉 )
29	3 28	syl	⊢ ( 𝜑 → ( ℩ 𝑎 ∈ 𝑉 𝑋 = 𝐴 ) ∈ 𝑉 )
30	1 29	eqeltrid	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
31		nfv	⊢ Ⅎ 𝑎 𝐼 ∈ 𝑉
32		nfcvd	⊢ ( 𝐼 ∈ 𝑉 → Ⅎ 𝑎 𝐼 )
33		nfcvd	⊢ ( 𝐼 ∈ 𝑉 → Ⅎ 𝑎 𝑌 )
34	32	nfcsb1d	⊢ ( 𝐼 ∈ 𝑉 → Ⅎ 𝑎 ⦋ 𝐼 / 𝑎 ⦌ 𝐴 )
35	33 34	nfeqd	⊢ ( 𝐼 ∈ 𝑉 → Ⅎ 𝑎 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 )
36		id	⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉 )
37		csbeq1a	⊢ ( 𝑎 = 𝐼 → 𝐴 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 )
38	37	eqeq2d	⊢ ( 𝑎 = 𝐼 → ( 𝑌 = 𝐴 ↔ 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ) )
39	38	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑎 = 𝐼 ) → ( 𝑌 = 𝐴 ↔ 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ) )
40	31 32 35 36 39	riota2df	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ∃! 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) → ( 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ↔ ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) = 𝐼 ) )
41	30 4 40	syl2anc	⊢ ( 𝜑 → ( 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ↔ ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) = 𝐼 ) )
42		eqcom	⊢ ( ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) = 𝐼 ↔ 𝐼 = ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) )
43	41 42	bitrdi	⊢ ( 𝜑 → ( 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ↔ 𝐼 = ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) ) )
44	43	adantr	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → ( 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ↔ 𝐼 = ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) ) )
45		csbeq1	⊢ ( 𝐽 = 𝐼 → ⦋ 𝐽 / 𝑎 ⦌ 𝐴 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 )
46	45	eqcoms	⊢ ( 𝐼 = 𝐽 → ⦋ 𝐽 / 𝑎 ⦌ 𝐴 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 )
47		eqeq12	⊢ ( ( 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ∧ 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ) → ( 𝑋 = 𝑌 ↔ ⦋ 𝐽 / 𝑎 ⦌ 𝐴 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ) )
48	47	ancoms	⊢ ( ( 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ∧ 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ) → ( 𝑋 = 𝑌 ↔ ⦋ 𝐽 / 𝑎 ⦌ 𝐴 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ) )
49	46 48	syl5ibrcom	⊢ ( 𝐼 = 𝐽 → ( ( 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ∧ 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ) → 𝑋 = 𝑌 ) )
50	49	expd	⊢ ( 𝐼 = 𝐽 → ( 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 → ( 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 → 𝑋 = 𝑌 ) ) )
51	50	adantl	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → ( 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 → ( 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 → 𝑋 = 𝑌 ) ) )
52	44 51	sylbird	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → ( 𝐼 = ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) → ( 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 → 𝑋 = 𝑌 ) ) )
53	9 27 52	mp2d	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → 𝑋 = 𝑌 )