Metamath Proof Explorer


Theorem uniabio

Description: Part of Theorem 8.17 in Quine p. 56. This theorem serves as a lemma for the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011)

Ref Expression
Assertion uniabio
|- ( A. x ( ph <-> x = y ) -> U. { x | ph } = y )

Proof

Step Hyp Ref Expression
1 abbi1
 |-  ( A. x ( ph <-> x = y ) -> { x | ph } = { x | x = y } )
2 df-sn
 |-  { y } = { x | x = y }
3 1 2 eqtr4di
 |-  ( A. x ( ph <-> x = y ) -> { x | ph } = { y } )
4 3 unieqd
 |-  ( A. x ( ph <-> x = y ) -> U. { x | ph } = U. { y } )
5 vex
 |-  y e. _V
6 5 unisn
 |-  U. { y } = y
7 4 6 eqtrdi
 |-  ( A. x ( ph <-> x = y ) -> U. { x | ph } = y )