Theorem reuunixfr 2901

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 2900 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 2899	. . . 4 |- (E!x e. A ph <-> E!y e. A ps)
5		reucl2 2883	. . . . 5 |- (E!y e. A ps -> U.{y e. A | ps} e. {y e. A | ps})
6		reucl 2880	. . . . . 6 |- (E!y e. A ps -> U.{y e. A | ps} e. A)
7		hbrab1 1769	. . . . . . . 8 |- (z e. {y e. A | ps} -> A.y z e. {y e. A | ps})
8	7	hbuni 2504	. . . . . . 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 2897	. . . . . 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 969	. . . . 5 |- (z e. C -> A.x z e. C)
16		hbrab1 1769	. . . . . . 7 |- (z e. {x e. A | ph} -> A.x z e. {x e. A | ph})
17	15, 16	hbel 1563	. . . . . 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 1531	. . . . 5 |- (x = C -> (x e. {x e. A | ph} <-> C e. {x e. A | ph}))
20	15, 18, 19	reuuni2f 2878	. . . 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 1766	. . . . . . 7 |- (x e. {x e. A | ph} <-> (x e. A /\ ph))
25	24	baibr 685	. . . . . 6 |- (x e. A -> (ph <-> x e. {x e. A | ph}))
26	25	reubiia 1778	. . . . 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 684	. . . 4 |- (x e. A -> (x e. {x e. A | ph} <-> ph))
31	30	rabbii 1801	. . 3 |- {x e. A | x e. {x e. A | ph}} = {x e. A | ph}
32	31	unieqi 2506	. 2 |- U.{x e. A | x e. {x e. A | ph}} = U.{x e. A | ph}
33	29, 32	syl5eqr 1518	1 |- (E!x e. A ph -> U.{x e. A | ph} = C)

Syntax hints:   -> wi 3   <-> wb 146  A.wal 952   = wceq 954   e. wcel 956  E!wreu 1644  {crab 1645  U.cuni 2498

This theorem is referenced by:  reuunineg 6021

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-un 2861

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-reu 1648  df-rab 1649  df-v 1808  df-sbc 1938  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-uni 2499

Copyright terms: Public domain