Theorem reu6 3288

Description: A way to express restricted uniqueness. (Contributed by NM, 20-Oct-2006.)

Assertion

Ref	Expression
reu6

Distinct variable groups:   ,,   ,

Proof of Theorem reu6

Step	Hyp	Ref	Expression
1		df-reu 2814	. 2
2		19.28v 1767	. . . . 5
3		eleq1 2529	. . . . . . . . . . . 12
4		sbequ12 1992	. . . . . . . . . . . 12
5	3, 4	anbi12d 710	. . . . . . . . . . 11
6		equequ1 1798	. . . . . . . . . . 11
7	5, 6	bibi12d 321	. . . . . . . . . 10
8		equid 1791	. . . . . . . . . . . 12
9	8	tbt 344	. . . . . . . . . . 11
10		simpl 457	. . . . . . . . . . 11
11	9, 10	sylbir 213	. . . . . . . . . 10
12	7, 11	syl6bi 228	. . . . . . . . 9
13	12	spimv 2009	. . . . . . . 8
14		bi1 186	. . . . . . . . . . . 12
15	14	expdimp 437	. . . . . . . . . . 11
16		bi2 198	. . . . . . . . . . . . 13
17		simpr 461	. . . . . . . . . . . . 13
18	16, 17	syl6 33	. . . . . . . . . . . 12
19	18	adantr 465	. . . . . . . . . . 11
20	15, 19	impbid 191	. . . . . . . . . 10
21	20	ex 434	. . . . . . . . 9
22	21	sps 1865	. . . . . . . 8
23	13, 22	jca 532	. . . . . . 7
24	23	axc4i 1898	. . . . . 6
25		bi1 186	. . . . . . . . . . 11
26	25	imim2i 14	. . . . . . . . . 10
27	26	impd 431	. . . . . . . . 9
28	27	adantl 466	. . . . . . . 8
29		eleq1a 2540	. . . . . . . . . . . 12
30	29	adantr 465	. . . . . . . . . . 11
31	30	imp 429	. . . . . . . . . 10
32		bi2 198	. . . . . . . . . . . . . 14
33	32	imim2i 14	. . . . . . . . . . . . 13
34	33	com23 78	. . . . . . . . . . . 12
35	34	imp 429	. . . . . . . . . . 11
36	35	adantll 713	. . . . . . . . . 10
37	31, 36	jcai 536	. . . . . . . . 9
38	37	ex 434	. . . . . . . 8
39	28, 38	impbid 191	. . . . . . 7
40	39	alimi 1633	. . . . . 6
41	24, 40	impbii 188	. . . . 5
42		df-ral 2812	. . . . . 6
43	42	anbi2i 694	. . . . 5
44	2, 41, 43	3bitr4i 277	. . . 4
45	44	exbii 1667	. . 3
46		df-eu 2286	. . 3
47		df-rex 2813	. . 3
48	45, 46, 47	3bitr4i 277	. 2
49	1, 48	bitri 249	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  E.wex 1612  [wsb 1739  e.wcel 1818  E!weu 2282  A.wral 2807  E.wrex 2808  E!wreu 2809

This theorem is referenced by:  reu3  3289  reu6i  3290  reu8  3295  xpf1o  7699  ufileu  20420  isppw2  23389  cusgrafilem2  24480  fgreu  27513  fcnvgreu  27514  fourierdlem50  31939

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-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-cleq 2449  df-clel 2452  df-ral 2812  df-rex 2813  df-reu 2814