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.

Step	Hyp	Ref	Expression
1		dfiota2 5557	. 2
2		vex 3112	. . . . . . 7
3		sbeqalb 3384	. . . . . . . 8
4		equcomi 1793	. . . . . . . 8
5	3, 4	syl6 33	. . . . . . 7
6	2, 5	ax-mp 5	. . . . . 6
7	6	ex 434	. . . . 5
8		equequ2 1799	. . . . . . . . . 10
9	8	equcoms 1795	. . . . . . . . 9
10	9	bibi2d 318	. . . . . . . 8
11	10	biimpd 207	. . . . . . 7
12	11	alimdv 1709	. . . . . 6
13	12	com12 31	. . . . 5
14	7, 13	impbid 191	. . . 4
15	14	alrimiv 1719	. . 3
16		uniabio 5566	. . 3
17	15, 16	syl 16	. 2
18	1, 17	syl5eq 2510	1

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