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 = ( iota_ a e. V X = A )
riotaeqimp.j 
|- J = ( iota_ a e. V Y = A )
riotaeqimp.x 
|- ( ph -> E! a e. V X = A )
riotaeqimp.y 
|- ( ph -> E! a e. V Y = A )
Assertion riotaeqimp 
|- ( ( ph /\ I = J ) -> X = Y )

Proof

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