Theorem reuunixfr 2906

Description: Change the variable x in the expression for "the unique A such that ph" to another variable y contained in expression B. Use reuhyp 2905 to eliminate the last hypothesis.

Hypotheses

Ref	Expression
reuunixfr.1	|- (z e. C -> A.y z e. C)
reuunixfr.2	|- (y e. A -> B e. A)
reuunixfr.3	|- (U.{y e. A | ps} e. A -> C e. A)
reuunixfr.4	|- (x = B -> (ph <-> ps))
reuunixfr.5	|- (y = U.{y e. A | ps} -> B = C)
reuunixfr.6	|- (x e. A -> E!y e. A x = B)

Assertion

Ref	Expression
reuunixfr	|- (E!x e. A ph -> U.{x e. A | ph} = C)

Distinct variable groups:   x,B   x,z,C   x,y,A,z   ph,y,z   ps,x,z

Proof of Theorem reuunixfr

Step	Hyp	Ref	Expression
1		reuunixfr.2	. . . . 5 |- (y e. A -> B e. A)
2		reuunixfr.6	. . . . 5 |- (x e. A -> E!y e. A x = B)
3		reuunixfr.4	. . . . 5 |- (x = B -> (ph <-> ps))
4	1, 2, 3	reuxfr 2904	. . . 4 |- (E!x e. A ph <-> E!y e. A ps)
5		reucl2 2888	. . . . 5 |- (E!y e. A ps -> U.{y e. A | ps} e. {y e. A | ps})
6		reucl 2885	. . . . . 6 |- (E!y e. A ps -> U.{y e. A | ps} e. A)
7		hbrab1 1772	. . . . . . . 8 |- (z e. {y e. A | ps} -> A.y z e. {y e. A | ps})
8	7	hbuni 2509	. . . . . . 7 |- (z e. U.{y e. A | ps} -> A.y z e. U.{y e. A | ps})
9		reuunixfr.1	. . . . . . 7 |- (z e. C -> A.y z e. C)
10		reuunixfr.5	. . . . . . 7 |- (y = U.{y e. A | ps} -> B = C)
11	8, 9, 1, 3, 10	rabxfr 2902	. . . . . 6 |- (U.{y e. A | ps} e. A -> (C e. {x e. A | ph} <-> U.{y e. A | ps} e. {y e. A | ps}))
12	6, 11	syl 10	. . . . 5 |- (E!y e. A ps -> (C e. {x e. A | ph} <-> U.{y e. A | ps} e. {y e. A | ps}))
13	5, 12	mpbird 196	. . . 4 |- (E!y e. A ps -> C e. {x e. A | ph})
14	4, 13	sylbi 199	. . 3 |- (E!x e. A ph -> C e. {x e. A | ph})
15		ax-17 971	. . . . 5 |- (z e. C -> A.x z e. C)
16		hbrab1 1772	. . . . . . 7 |- (z e. {x e. A | ph} -> A.x z e. {x e. A | ph})
17	15, 16	hbel 1566	. . . . . 6 |- (C e. {x e. A | ph} -> A.x C e. {x e. A | ph})
18	17	a1i 8	. . . . 5 |- (C e. A -> (C e. {x e. A | ph} -> A.x C e. {x e. A | ph}))
19		eleq1 1534	. . . . 5 |- (x = C -> (x e. {x e. A | ph} <-> C e. {x e. A | ph}))
20	15, 18, 19	reuuni2f 2883	. . . 4 |- ((C e. A /\ E!x e. A x e. {x e. A | ph}) -> (C e. {x e. A | ph} <-> U.{x e. A | x e. {x e. A | ph}} = C))
21		reuunixfr.3	. . . . . 6 |- (U.{y e. A | ps} e. A -> C e. A)
22	6, 21	syl 10	. . . . 5 |- (E!y e. A ps -> C e. A)
23	4, 22	sylbi 199	. . . 4 |- (E!x e. A ph -> C e. A)
24		rabid 1769	. . . . . . 7 |- (x e. {x e. A | ph} <-> (x e. A /\ ph))
25	24	baibr 686	. . . . . 6 |- (x e. A -> (ph <-> x e. {x e. A | ph}))
26	25	reubiia 1781	. . . . 5 |- (E!x e. A ph <-> E!x e. A x e. {x e. A | ph})
27	26	biimp 151	. . . 4 |- (E!x e. A ph -> E!x e. A x e. {x e. A | ph})
28	20, 23, 27	sylanc 471	. . 3 |- (E!x e. A ph -> (C e. {x e. A | ph} <-> U.{x e. A | x e. {x e. A | ph}} = C))
29	14, 28	mpbid 195	. 2 |- (E!x e. A ph -> U.{x e. A | x e. {x e. A | ph}} = C)
30	24	baib 685	. . . 4 |- (x e. A -> (x e. {x e. A | ph} <-> ph))
31	30	rabbii 1805	. . 3 |- {x e. A | x e. {x e. A | ph}} = {x e. A | ph}
32	31	unieqi 2511	. 2 |- U.{x e. A | x e. {x e. A | ph}} = U.{x e. A | ph}
33	29, 32	syl5eqr 1521	1 |- (E!x e. A ph -> U.{x e. A | ph} = C)

Syntax hints:   -> wi 3   <-> wb 146  A.wal 954   = wceq 956   e. wcel 958  E!wreu 1647  {crab 1648  U.cuni 2503

This theorem is referenced by:  reuunineg 6066

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 777  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-reu 1651  df-rab 1652  df-v 1812  df-sbc 1942  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-uni 2504

Copyright terms: Public domain