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

Theorem iotaval 5567
 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
Distinct variable group:   ,

Proof of Theorem iotaval
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dfiota2 5557 . 2
2 vex 3112 . . . . . . 7
3 sbeqalb 3384 . . . . . . . 8
4 equcomi 1793 . . . . . . . 8
53, 4syl6 33 . . . . . . 7
62, 5ax-mp 5 . . . . . 6
76ex 434 . . . . 5
8 equequ2 1799 . . . . . . . . . 10
98equcoms 1795 . . . . . . . . 9
109bibi2d 318 . . . . . . . 8
1110biimpd 207 . . . . . . 7
1211alimdv 1709 . . . . . 6
1312com12 31 . . . . 5
147, 13impbid 191 . . . 4
1514alrimiv 1719 . . 3
16 uniabio 5566 . . 3
1715, 16syl 16 . 2
181, 17syl5eq 2510 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  =wceq 1395  e.wcel 1818  {cab 2442   cvv 3109  U.cuni 4249  iotacio 5554 This theorem is referenced by:  iotauni  5568  iota1  5570  iotaex  5573  iota4  5574  iota5  5576  iota5f  29102  iotain  31324  iotaexeu  31325  iotasbc  31326  iotaequ  31336  iotavalb  31337  pm14.24  31339  sbiota1  31341 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-v 3111  df-sbc 3328  df-un 3480  df-sn 4030  df-pr 4032  df-uni 4250  df-iota 5556
 Copyright terms: Public domain W3C validator