MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iotaval Unicode version

Theorem iotaval 5392
Description: Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.)
Assertion
Ref Expression
iotaval  |-  ( A. x ( ph  <->  x  =  y )  ->  ( iota x ph )  =  y )
Distinct variable group:    x, y
Allowed substitution hints:    ph( x, y)

Proof of Theorem iotaval
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 dfiota2 5382 . 2  |-  ( iota
x ph )  =  U. { z  |  A. x ( ph  <->  x  =  z ) }
2 vex 2923 . . . . . . 7  |-  y  e. 
_V
3 sbeqalb 3177 . . . . . . . 8  |-  ( y  e.  _V  ->  (
( A. x (
ph 
<->  x  =  y )  /\  A. x (
ph 
<->  x  =  z ) )  ->  y  =  z ) )
4 equcomi 1687 . . . . . . . 8  |-  ( y  =  z  ->  z  =  y )
53, 4syl6 31 . . . . . . 7  |-  ( y  e.  _V  ->  (
( A. x (
ph 
<->  x  =  y )  /\  A. x (
ph 
<->  x  =  z ) )  ->  z  =  y ) )
62, 5ax-mp 8 . . . . . 6  |-  ( ( A. x ( ph  <->  x  =  y )  /\  A. x ( ph  <->  x  =  z ) )  -> 
z  =  y )
76ex 424 . . . . 5  |-  ( A. x ( ph  <->  x  =  y )  ->  ( A. x ( ph  <->  x  =  z )  ->  z  =  y ) )
8 equequ2 1694 . . . . . . . . . 10  |-  ( y  =  z  ->  (
x  =  y  <->  x  =  z ) )
98equcoms 1689 . . . . . . . . 9  |-  ( z  =  y  ->  (
x  =  y  <->  x  =  z ) )
109bibi2d 310 . . . . . . . 8  |-  ( z  =  y  ->  (
( ph  <->  x  =  y
)  <->  ( ph  <->  x  =  z ) ) )
1110biimpd 199 . . . . . . 7  |-  ( z  =  y  ->  (
( ph  <->  x  =  y
)  ->  ( ph  <->  x  =  z ) ) )
1211alimdv 1628 . . . . . 6  |-  ( z  =  y  ->  ( A. x ( ph  <->  x  =  y )  ->  A. x
( ph  <->  x  =  z
) ) )
1312com12 29 . . . . 5  |-  ( A. x ( ph  <->  x  =  y )  ->  (
z  =  y  ->  A. x ( ph  <->  x  =  z ) ) )
147, 13impbid 184 . . . 4  |-  ( A. x ( ph  <->  x  =  y )  ->  ( A. x ( ph  <->  x  =  z )  <->  z  =  y ) )
1514alrimiv 1638 . . 3  |-  ( A. x ( ph  <->  x  =  y )  ->  A. z
( A. x (
ph 
<->  x  =  z )  <-> 
z  =  y ) )
16 uniabio 5391 . . 3  |-  ( A. z ( A. x
( ph  <->  x  =  z
)  <->  z  =  y )  ->  U. { z  |  A. x (
ph 
<->  x  =  z ) }  =  y )
1715, 16syl 16 . 2  |-  ( A. x ( ph  <->  x  =  y )  ->  U. {
z  |  A. x
( ph  <->  x  =  z
) }  =  y )
181, 17syl5eq 2452 1  |-  ( A. x ( ph  <->  x  =  y )  ->  ( iota x ph )  =  y )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1546    = wceq 1649    e. wcel 1721   {cab 2394   _Vcvv 2920   U.cuni 3979   iotacio 5379
This theorem is referenced by:  iotauni  5393  iota1  5395  iotaex  5398  iota4  5399  iota5  5401  iota5f  25139  iotain  27489  iotaexeu  27490  iotasbc  27491  iotaequ  27501  iotavalb  27502  pm14.24  27504  sbiota1  27506
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-rex 2676  df-v 2922  df-sbc 3126  df-un 3289  df-sn 3784  df-pr 3785  df-uni 3980  df-iota 5381
  Copyright terms: Public domain W3C validator