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

Metamath Proof Explorer

Theorem iotaval2

Description: Version of iotaval using df-iota instead of dfiota2 . (Contributed by SN, 6-Nov-2024)

Ref Expression
Assertion iotaval2 
|- ( { x | ph } = { y } -> ( iota x ph ) = y )

Proof

Step Hyp Ref Expression
1 df-iota 
 |-  ( iota x ph ) = U. { w | { x | ph } = { w } }
2 eqeq1 
 |-  ( { x | ph } = { y } -> ( { x | ph } = { w } <-> { y } = { w } ) )
3 sneqbg 
 |-  ( y e. _V -> ( { y } = { w } <-> y = w ) )
4 3 elv 
 |-  ( { y } = { w } <-> y = w )
5 equcom 
 |-  ( y = w <-> w = y )
6 4 5 bitri 
 |-  ( { y } = { w } <-> w = y )
7 2 6 bitrdi 
 |-  ( { x | ph } = { y } -> ( { x | ph } = { w } <-> w = y ) )
8 7 alrimiv 
 |-  ( { x | ph } = { y } -> A. w ( { x | ph } = { w } <-> w = y ) )
9 uniabio 
 |-  ( A. w ( { x | ph } = { w } <-> w = y ) -> U. { w | { x | ph } = { w } } = y )
10 8 9 syl 
 |-  ( { x | ph } = { y } -> U. { w | { x | ph } = { w } } = y )
11 1 10 eqtrid 
 |-  ( { x | ph } = { y } -> ( iota x ph ) = y )