# 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 ) )`