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

Metamath Proof Explorer

Theorem iotaeq

Description: Equality theorem for descriptions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Andrew Salmon, 30-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion iotaeq 
|- ( A. x x = y -> ( iota x ph ) = ( iota y ph ) )

Proof

Step Hyp Ref Expression
1 drsb1 
 |-  ( A. x x = y -> ( [ z / x ] ph <-> [ z / y ] ph ) )
2 df-clab 
 |-  ( z e. { x | ph } <-> [ z / x ] ph )
3 df-clab 
 |-  ( z e. { y | ph } <-> [ z / y ] ph )
4 1 2 3 3bitr4g 
 |-  ( A. x x = y -> ( z e. { x | ph } <-> z e. { y | ph } ) )
5 4 eqrdv 
 |-  ( A. x x = y -> { x | ph } = { y | ph } )
6 5 eqeq1d 
 |-  ( A. x x = y -> ( { x | ph } = { z } <-> { y | ph } = { z } ) )
7 6 abbidv 
 |-  ( A. x x = y -> { z | { x | ph } = { z } } = { z | { y | ph } = { z } } )
8 7 unieqd 
 |-  ( A. x x = y -> U. { z | { x | ph } = { z } } = U. { z | { y | ph } = { z } } )
9 df-iota 
 |-  ( iota x ph ) = U. { z | { x | ph } = { z } }
10 df-iota 
 |-  ( iota y ph ) = U. { z | { y | ph } = { z } }
11 8 9 10 3eqtr4g 
 |-  ( A. x x = y -> ( iota x ph ) = ( iota y ph ) )