Theorem reuunixfr 3850

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 3849 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 3847	. . . 4 |- (E!x e. A ph <-> E!y e. A ps)
5		reucl2 3814	. . . . 5 |- (E!y e. A ps -> U.{y e. A | ps} e. {y e. A | ps})
6		reucl 3213	. . . . . 6 |- (E!y e. A ps -> U.{y e. A | ps} e. A)
7		hbrab1 2257	. . . . . . . 8 |- (z e. {y e. A | ps} -> A.y z e. {y e. A | ps})
8	7	hbuni 3183	. . . . . . 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 3843	. . . . . 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 12	. . . . 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 213	. . . 4 |- (E!y e. A ps -> C e. {x e. A | ph})
14	4, 13	sylbi 216	. . 3 |- (E!x e. A ph -> C e. {x e. A | ph})
15		reuunixfr.3	. . . . . 6 |- (U.{y e. A | ps} e. A -> C e. A)
16	6, 15	syl 12	. . . . 5 |- (E!y e. A ps -> C e. A)
17	4, 16	sylbi 216	. . . 4 |- (E!x e. A ph -> C e. A)
18		rabid 2253	. . . . . . 7 |- (x e. {x e. A | ph} <-> (x e. A /\ ph))
19	18	baibr 750	. . . . . 6 |- (x e. A -> (ph <-> x e. {x e. A | ph}))
20	19	reubiia 2261	. . . . 5 |- (E!x e. A ph <-> E!x e. A x e. {x e. A | ph})
21	20	biimpi 168	. . . 4 |- (E!x e. A ph -> E!x e. A x e. {x e. A | ph})
22		ax-17 1317	. . . . 5 |- (z e. C -> A.x z e. C)
23		hbrab1 2257	. . . . . . 7 |- (z e. {x e. A | ph} -> A.x z e. {x e. A | ph})
24	22, 23	hbel 1996	. . . . . 6 |- (C e. {x e. A | ph} -> A.x C e. {x e. A | ph})
25	24	a1i 8	. . . . 5 |- (C e. A -> (C e. {x e. A | ph} -> A.x C e. {x e. A | ph}))
26		eleq1 1957	. . . . 5 |- (x = C -> (x e. {x e. A | ph} <-> C e. {x e. A | ph}))
27	22, 25, 26	reuuni2f 3810	. . . 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))
28	17, 21, 27	syl11anc 524	. . 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 212	. 2 |- (E!x e. A ph -> U.{x e. A | x e. {x e. A | ph}} = C)
30	18	baib 749	. . . 4 |- (x e. A -> (x e. {x e. A | ph} <-> ph))
31	30	rabbiia 2285	. . 3 |- {x e. A | x e. {x e. A | ph}} = {x e. A | ph}
32	31	unieqi 3187	. 2 |- U.{x e. A | x e. {x e. A | ph}} = U.{x e. A | ph}
33	29, 32	syl5eqr 1942	1 |- (E!x e. A ph -> U.{x e. A | ph} = C)

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296   = wceq 1298   e. wcel 1300  E!wreu 2107  {crab 2108  U.cuni 3177

This theorem is referenced by:  reuunineg 7275

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-uni 3178

Copyright terms: Public domain