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 a1i 
 |-  ( ph -> ( I = ( iota_ a e. V Y = A ) <-> I = J ) )
8 7 bicomd 
 |-  ( ph -> ( I = J <-> I = ( iota_ a e. V Y = A ) ) )
9 8 biimpa 
 |-  ( ( ph /\ I = J ) -> I = ( iota_ a e. V Y = A ) )
10 1 eqeq1i 
 |-  ( I = J <-> ( iota_ a e. V X = A ) = J )
11 riotacl 
 |-  ( E! a e. V Y = A -> ( iota_ a e. V Y = A ) e. V )
12 4 11 syl 
 |-  ( ph -> ( iota_ a e. V Y = A ) e. V )
13 2 12 eqeltrid 
 |-  ( ph -> J e. V )
14 nfv 
 |-  F/ a J e. V
15 nfcvd 
 |-  ( J e. V -> F/_ a J )
16 nfcvd 
 |-  ( J e. V -> F/_ a X )
17 15 nfcsb1d 
 |-  ( J e. V -> F/_ a [_ J / a ]_ A )
18 16 17 nfeqd 
 |-  ( J e. V -> F/ a X = [_ J / a ]_ A )
19 id 
 |-  ( J e. V -> J e. V )
20 csbeq1a 
 |-  ( a = J -> A = [_ J / a ]_ A )
21 20 eqeq2d 
 |-  ( a = J -> ( X = A <-> X = [_ J / a ]_ A ) )
22 21 adantl 
 |-  ( ( J e. V /\ a = J ) -> ( X = A <-> X = [_ J / a ]_ A ) )
23 14 15 18 19 22 riota2df 
 |-  ( ( J e. V /\ E! a e. V X = A ) -> ( X = [_ J / a ]_ A <-> ( iota_ a e. V X = A ) = J ) )
24 23 bicomd 
 |-  ( ( J e. V /\ E! a e. V X = A ) -> ( ( iota_ a e. V X = A ) = J <-> X = [_ J / a ]_ A ) )
25 13 3 24 syl2anc 
 |-  ( ph -> ( ( iota_ a e. V X = A ) = J <-> X = [_ J / a ]_ A ) )
26 10 25 bitrid 
 |-  ( ph -> ( I = J <-> X = [_ J / a ]_ A ) )
27 26 biimpa 
 |-  ( ( ph /\ I = J ) -> X = [_ J / a ]_ A )
28 riotacl 
 |-  ( E! a e. V X = A -> ( iota_ a e. V X = A ) e. V )
29 3 28 syl 
 |-  ( ph -> ( iota_ a e. V X = A ) e. V )
30 1 29 eqeltrid 
 |-  ( ph -> I e. V )
31 nfv 
 |-  F/ a I e. V
32 nfcvd 
 |-  ( I e. V -> F/_ a I )
33 nfcvd 
 |-  ( I e. V -> F/_ a Y )
34 32 nfcsb1d 
 |-  ( I e. V -> F/_ a [_ I / a ]_ A )
35 33 34 nfeqd 
 |-  ( I e. V -> F/ a Y = [_ I / a ]_ A )
36 id 
 |-  ( I e. V -> I e. V )
37 csbeq1a 
 |-  ( a = I -> A = [_ I / a ]_ A )
38 37 eqeq2d 
 |-  ( a = I -> ( Y = A <-> Y = [_ I / a ]_ A ) )
39 38 adantl 
 |-  ( ( I e. V /\ a = I ) -> ( Y = A <-> Y = [_ I / a ]_ A ) )
40 31 32 35 36 39 riota2df 
 |-  ( ( I e. V /\ E! a e. V Y = A ) -> ( Y = [_ I / a ]_ A <-> ( iota_ a e. V Y = A ) = I ) )
41 30 4 40 syl2anc 
 |-  ( ph -> ( Y = [_ I / a ]_ A <-> ( iota_ a e. V Y = A ) = I ) )
42 eqcom 
 |-  ( ( iota_ a e. V Y = A ) = I <-> I = ( iota_ a e. V Y = A ) )
43 41 42 bitrdi 
 |-  ( ph -> ( Y = [_ I / a ]_ A <-> I = ( iota_ a e. V Y = A ) ) )
44 43 adantr 
 |-  ( ( ph /\ I = J ) -> ( Y = [_ I / a ]_ A <-> I = ( iota_ a e. 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 
 |-  ( ( ph /\ I = J ) -> ( Y = [_ I / a ]_ A -> ( X = [_ J / a ]_ A -> X = Y ) ) )
52 44 51 sylbird 
 |-  ( ( ph /\ I = J ) -> ( I = ( iota_ a e. V Y = A ) -> ( X = [_ J / a ]_ A -> X = Y ) ) )
53 9 27 52 mp2d 
 |-  ( ( ph /\ I = J ) -> X = Y )