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

Theorem iotaex 5496
Description: Theorem 8.23 in [Quine] p. 58. This theorem proves the existence of the  iota class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011.)
Assertion
Ref Expression
iotaex  |-  ( iota
x ph )  e.  _V

Proof of Theorem iotaex
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 iotaval 5490 . . . . 5  |-  ( A. x ( ph  <->  x  =  z )  ->  ( iota x ph )  =  z )
21eqcomd 2459 . . . 4  |-  ( A. x ( ph  <->  x  =  z )  ->  z  =  ( iota x ph ) )
32eximi 1626 . . 3  |-  ( E. z A. x (
ph 
<->  x  =  z )  ->  E. z  z  =  ( iota x ph ) )
4 df-eu 2264 . . 3  |-  ( E! x ph  <->  E. z A. x ( ph  <->  x  =  z ) )
5 isset 3072 . . 3  |-  ( ( iota x ph )  e.  _V  <->  E. z  z  =  ( iota x ph ) )
63, 4, 53imtr4i 266 . 2  |-  ( E! x ph  ->  ( iota x ph )  e. 
_V )
7 iotanul 5494 . . 3  |-  ( -.  E! x ph  ->  ( iota x ph )  =  (/) )
8 0ex 4520 . . 3  |-  (/)  e.  _V
97, 8syl6eqel 2547 . 2  |-  ( -.  E! x ph  ->  ( iota x ph )  e.  _V )
106, 9pm2.61i 164 1  |-  ( iota
x ph )  e.  _V
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184   A.wal 1368    = wceq 1370   E.wex 1587    e. wcel 1758   E!weu 2260   _Vcvv 3068   (/)c0 3735   iotacio 5477
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-nul 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-sn 3976  df-pr 3978  df-uni 4190  df-iota 5479
This theorem is referenced by:  iota4an  5498  fvex  5799  riotaex  6155  erov  7297  iunfictbso  8385  isf32lem9  8631  sumex  13267  pcval  14013  grpidval  15534  fn0g  15535  gsumvalx  15604  psgnfn  16109  psgnval  16115  dchrptlem1  22719  lgsdchrval  22802  lgsdchr  22803  prodex  27554  bnj1366  32123  bj-finsumval0  32889
  Copyright terms: Public domain W3C validator