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 syl5bb
 |-  ( 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 )