Theorem reuuni4 3110

Description: Derive the property of "the unique element in A such that ph" when expressed explicitly as U.{x e. A | ph}.

Assertion

Ref	Expression
reuuni4	|- (E!x e. A ph -> [U.{x e. A | ph} / x]ph)

Distinct variable group:   x,A

Proof of Theorem reuuni4

Step	Hyp	Ref	Expression
1		reucl 2584	. 2 |- (E!x e. A ph -> U.{x e. A | ph} e. A)
2		reurex 1974	. . . 4 |- (E!x e. A ph -> E.x e. A ph)
3		hbreu1 1814	. . . . 5 |- (E!x e. A ph -> A.xE!x e. A ph)
4		hbrab1 1818	. . . . . . 7 |- (y e. {x e. A | ph} -> A.x y e. {x e. A | ph})
5	4	hbuni 2575	. . . . . 6 |- (y e. U.{x e. A | ph} -> A.x y e. U.{x e. A | ph})
6	5	hbsbc1 1994	. . . . 5 |- ((U.{x e. A | ph} e. V -> [U.{x e. A | ph} / x]ph) -> A.x(U.{x e. A | ph} e. V -> [U.{x e. A | ph} / x]ph))
7		reuuni1 3106	. . . . . . . . . 10 |- ((x e. A /\ E!x e. A ph) -> (ph <-> U.{x e. A | ph} = x))
8		sbceq1a 1989	. . . . . . . . . . 11 |- (x = U.{x e. A | ph} -> (ph <-> [U.{x e. A | ph} / x]ph))
9	8	eqcoms 1521	. . . . . . . . . 10 |- (U.{x e. A | ph} = x -> (ph <-> [U.{x e. A | ph} / x]ph))
10	7, 9	syl6bi 212	. . . . . . . . 9 |- ((x e. A /\ E!x e. A ph) -> (ph -> (ph <-> [U.{x e. A | ph} / x]ph)))
11	10	ibd 597	. . . . . . . 8 |- ((x e. A /\ E!x e. A ph) -> (ph -> [U.{x e. A | ph} / x]ph))
12	11	expcom 372	. . . . . . 7 |- (E!x e. A ph -> (x e. A -> (ph -> [U.{x e. A | ph} / x]ph)))
13	12	a1i 8	. . . . . 6 |- (U.{x e. A | ph} e. V -> (E!x e. A ph -> (x e. A -> (ph -> [U.{x e. A | ph} / x]ph))))
14	13	com4l 39	. . . . 5 |- (E!x e. A ph -> (x e. A -> (ph -> (U.{x e. A | ph} e. V -> [U.{x e. A | ph} / x]ph))))
15	3, 6, 14	r19.23ad 1791	. . . 4 |- (E!x e. A ph -> (E.x e. A ph -> (U.{x e. A | ph} e. V -> [U.{x e. A | ph} / x]ph)))
16	2, 15	mpd 26	. . 3 |- (E!x e. A ph -> (U.{x e. A | ph} e. V -> [U.{x e. A | ph} / x]ph))
17		elisset 1863	. . 3 |- (U.{x e. A | ph} e. A -> U.{x e. A | ph} e. V)
18	16, 17	syl5 21	. 2 |- (E!x e. A ph -> (U.{x e. A | ph} e. A -> [U.{x e. A | ph} / x]ph))
19	1, 18	mpd 26	1 |- (E!x e. A ph -> [U.{x e. A | ph} / x]ph)

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221   = wceq 992   e. wcel 994  [wsbc 1207  E.wrex 1692  E!wreu 1693  {crab 1694  Vcvv 1857  U.cuni 2569

This theorem is referenced by:  reucl2 3111  reuuniss 3112  reuuniss2 3114  ordtypelem6 11432

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-rex 1696  df-reu 1697  df-rab 1698  df-v 1858  df-sbc 1987  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-uni 2570

Copyright terms: Public domain