This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvriota

Description: Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvriotaw when possible. (Contributed by NM, 18-Mar-2013) (Revised by Mario Carneiro, 15-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses cbvriota.1 
|- F/ y ph
cbvriota.2 
|- F/ x ps
cbvriota.3 
|- ( x = y -> ( ph <-> ps ) )
Assertion cbvriota 
|- ( iota_ x e. A ph ) = ( iota_ y e. A ps )

Proof

Step Hyp Ref Expression
1 cbvriota.1 
 |-  F/ y ph
2 cbvriota.2 
 |-  F/ x ps
3 cbvriota.3 
 |-  ( x = y -> ( ph <-> ps ) )
4 eleq1w 
 |-  ( x = z -> ( x e. A <-> z e. A ) )
5 sbequ12 
 |-  ( x = z -> ( ph <-> [ z / x ] ph ) )
6 4 5 anbi12d 
 |-  ( x = z -> ( ( x e. A /\ ph ) <-> ( z e. A /\ [ z / x ] ph ) ) )
7 nfv 
 |-  F/ z ( x e. A /\ ph )
8 nfv 
 |-  F/ x z e. A
9 nfs1v 
 |-  F/ x [ z / x ] ph
10 8 9 nfan 
 |-  F/ x ( z e. A /\ [ z / x ] ph )
11 6 7 10 cbviota 
 |-  ( iota x ( x e. A /\ ph ) ) = ( iota z ( z e. A /\ [ z / x ] ph ) )
12 eleq1w 
 |-  ( z = y -> ( z e. A <-> y e. A ) )
13 sbequ 
 |-  ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) )
14 2 3 sbie 
 |-  ( [ y / x ] ph <-> ps )
15 13 14 bitrdi 
 |-  ( z = y -> ( [ z / x ] ph <-> ps ) )
16 12 15 anbi12d 
 |-  ( z = y -> ( ( z e. A /\ [ z / x ] ph ) <-> ( y e. A /\ ps ) ) )
17 nfv 
 |-  F/ y z e. A
18 1 nfsb 
 |-  F/ y [ z / x ] ph
19 17 18 nfan 
 |-  F/ y ( z e. A /\ [ z / x ] ph )
20 nfv 
 |-  F/ z ( y e. A /\ ps )
21 16 19 20 cbviota 
 |-  ( iota z ( z e. A /\ [ z / x ] ph ) ) = ( iota y ( y e. A /\ ps ) )
22 11 21 eqtri 
 |-  ( iota x ( x e. A /\ ph ) ) = ( iota y ( y e. A /\ ps ) )
23 df-riota 
 |-  ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
24 df-riota 
 |-  ( iota_ y e. A ps ) = ( iota y ( y e. A /\ ps ) )
25 22 23 24 3eqtr4i 
 |-  ( iota_ x e. A ph ) = ( iota_ y e. A ps )