Metamath Proof Explorer


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 = ι a V | X = A
riotaeqimp.j J = ι a V | Y = A
riotaeqimp.x φ ∃! a V X = A
riotaeqimp.y φ ∃! a V Y = A
Assertion riotaeqimp φ I = J X = Y

Proof

Step Hyp Ref Expression
1 riotaeqimp.i I = ι a V | X = A
2 riotaeqimp.j J = ι a V | Y = A
3 riotaeqimp.x φ ∃! a V X = A
4 riotaeqimp.y φ ∃! a V Y = A
5 2 eqcomi ι a V | Y = A = J
6 5 eqeq2i I = ι a V | Y = A I = J
7 6 a1i φ I = ι a V | Y = A I = J
8 7 bicomd φ I = J I = ι a V | Y = A
9 8 biimpa φ I = J I = ι a V | Y = A
10 1 eqeq1i I = J ι a V | X = A = J
11 riotacl ∃! a V Y = A ι a V | Y = A V
12 4 11 syl φ ι a V | Y = A V
13 2 12 eqeltrid φ J V
14 nfv a J V
15 nfcvd J V _ a J
16 nfcvd J V _ a X
17 15 nfcsb1d J V _ a J / a A
18 16 17 nfeqd J V a X = J / a A
19 id J V J V
20 csbeq1a a = J A = J / a A
21 20 eqeq2d a = J X = A X = J / a A
22 21 adantl J V a = J X = A X = J / a A
23 14 15 18 19 22 riota2df J V ∃! a V X = A X = J / a A ι a V | X = A = J
24 23 bicomd J V ∃! a V X = A ι a V | X = A = J X = J / a A
25 13 3 24 syl2anc φ ι a V | X = A = J X = J / a A
26 10 25 syl5bb φ I = J X = J / a A
27 26 biimpa φ I = J X = J / a A
28 riotacl ∃! a V X = A ι a V | X = A V
29 3 28 syl φ ι a V | X = A V
30 1 29 eqeltrid φ I V
31 nfv a I V
32 nfcvd I V _ a I
33 nfcvd I V _ a Y
34 32 nfcsb1d I V _ a I / a A
35 33 34 nfeqd I V a Y = I / a A
36 id I V I V
37 csbeq1a a = I A = I / a A
38 37 eqeq2d a = I Y = A Y = I / a A
39 38 adantl I V a = I Y = A Y = I / a A
40 31 32 35 36 39 riota2df I V ∃! a V Y = A Y = I / a A ι a V | Y = A = I
41 30 4 40 syl2anc φ Y = I / a A ι a V | Y = A = I
42 eqcom ι a V | Y = A = I I = ι a V | Y = A
43 41 42 bitrdi φ Y = I / a A I = ι a V | Y = A
44 43 adantr φ I = J Y = I / a A I = ι a V | Y = A
45 csbeq1 J = I J / a A = I / a A
46 45 eqcoms I = J J / a A = I / a A
47 eqeq12 X = J / a A Y = I / a A X = Y J / a A = I / a A
48 47 ancoms Y = I / a A X = J / a A X = Y J / a A = I / a A
49 46 48 syl5ibrcom I = J Y = I / a A X = J / a A X = Y
50 49 expd I = J Y = I / a A X = J / a A X = Y
51 50 adantl φ I = J Y = I / a A X = J / a A X = Y
52 44 51 sylbird φ I = J I = ι a V | Y = A X = J / a A X = Y
53 9 27 52 mp2d φ I = J X = Y