Theorem dfiota2 4981

Description: Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.)

Assertion

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

Distinct variable groups:   x, y   ph, y

Allowed substitution hint:   ph( x)

Proof of Theorem dfiota2

Step	Hyp	Ref	Expression
1		df-iota 4980	. 2 |- ( iota x ph ) = U. { y | { x | ph } = { y } }
2		df-sn 3452	. . . . . 6 |- { y } = { x | x = y }
3	2	eqeq2i 2098	. . . . 5 |- ( { x | ph } = { y } <-> { x | ph } = { x | x = y } )
4		abbi 2201	. . . . 5 |- ( A. x ( ph <-> x = y ) <-> { x | ph } = { x | x = y } )
5	3, 4	bitr4i 185	. . . 4 |- ( { x | ph } = { y } <-> A. x ( ph <-> x = y ) )
6	5	abbii 2203	. . 3 |- { y | { x | ph } = { y } } = { y | A. x ( ph <-> x = y ) }
7	6	unieqi 3663	. 2 |- U. { y | { x | ph } = { y } } = U. { y | A. x ( ph <-> x = y ) }
8	1, 7	eqtri 2108	1 |- ( iota x ph ) = U. { y | A. x ( ph <-> x = y ) }

Syntax hints:   <-> wb 103   A.wal 1287   = wceq 1289   {cab 2074   {csn 3446   U.cuni 3653   iotacio 4978

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rex 2365  df-sn 3452  df-uni 3654  df-iota 4980

This theorem is referenced by:  nfiota1  4982  nfiotadxy  4983  cbviota  4985  sb8iota  4987  iotaval  4991  iotanul  4995  fv2  5300