Theorem reucl 3213

Description: Closure law for "the unique element in A such that ph."

Assertion

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

Distinct variable group:   x,A

Proof of Theorem reucl

Step	Hyp	Ref	Expression
1		euabsn 3095	. . 3 |- (E!x(x e. A /\ ph) <-> E.x{x | (x e. A /\ ph)} = {x})
2		hbab1 1874	. . . . . 6 |- (y e. {x | (x e. A /\ ph)} -> A.x y e. {x | (x e. A /\ ph)})
3	2	hbuni 3183	. . . . 5 |- (y e. U.{x | (x e. A /\ ph)} -> A.x y e. U.{x | (x e. A /\ ph)})
4		ax-17 1317	. . . . 5 |- (y e. A -> A.x y e. A)
5	3, 4	hbel 1996	. . . 4 |- (U.{x | (x e. A /\ ph)} e. A -> A.xU.{x | (x e. A /\ ph)} e. A)
6		unieq 3185	. . . . . 6 |- ({x | (x e. A /\ ph)} = {x} -> U.{x | (x e. A /\ ph)} = U.{x})
7		visset 2295	. . . . . . 7 |- x e. _V
8	7	unisn 3193	. . . . . 6 |- U.{x} = x
9	6, 8	syl6req 1945	. . . . 5 |- ({x | (x e. A /\ ph)} = {x} -> x = U.{x | (x e. A /\ ph)})
10	7	snid 3069	. . . . . . . 8 |- x e. {x}
11		eleq2 1958	. . . . . . . 8 |- ({x | (x e. A /\ ph)} = {x} -> (x e. {x | (x e. A /\ ph)} <-> x e. {x}))
12	10, 11	mpbiri 211	. . . . . . 7 |- ({x | (x e. A /\ ph)} = {x} -> x e. {x | (x e. A /\ ph)})
13		abid 1873	. . . . . . 7 |- (x e. {x | (x e. A /\ ph)} <-> (x e. A /\ ph))
14	12, 13	sylib 215	. . . . . 6 |- ({x | (x e. A /\ ph)} = {x} -> (x e. A /\ ph))
15	14	simplld 348	. . . . 5 |- ({x | (x e. A /\ ph)} = {x} -> x e. A)
16	9, 15	eqeltrrd 1972	. . . 4 |- ({x | (x e. A /\ ph)} = {x} -> U.{x | (x e. A /\ ph)} e. A)
17	5, 16	19.23ai 1412	. . 3 |- (E.x{x | (x e. A /\ ph)} = {x} -> U.{x | (x e. A /\ ph)} e. A)
18	1, 17	sylbi 216	. 2 |- (E!x(x e. A /\ ph) -> U.{x | (x e. A /\ ph)} e. A)
19		df-reu 2111	. 2 |- (E!x e. A ph <-> E!x(x e. A /\ ph))
20		df-rab 2112	. . . 4 |- {x e. A | ph} = {x | (x e. A /\ ph)}
21	20	unieqi 3187	. . 3 |- U.{x e. A | ph} = U.{x | (x e. A /\ ph)}
22	21	eleq1i 1960	. 2 |- (U.{x e. A | ph} e. A <-> U.{x | (x e. A /\ ph)} e. A)
23	18, 19, 22	3imtr4i 236	1 |- (E!x e. A ph -> U.{x e. A | ph} e. A)

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  E!weu 1771  {cab 1871  E!wreu 2107  {crab 2108  {csn 3044  U.cuni 3177

This theorem is referenced by:  wereucl 3655  reuuni3 3812  reuuni4 3813  reucl2 3814  reuuniss 3815  reuuniss2 3817  euexeqOLD 3826  euexaleq 3827  reuunixfr 3850  supcl 5669  hartog 5693  aceq6a 5903  uzwo3lem2 7430  flcl 7465  recl 8007  imcl 8008  isumcl 8470  grpidcl 9343  grpinvcl 9352  minveccl 9929  spwcl 10003  iorlid 10375  axpjcl 10873  cnlnadjlem3 11639  cnlnadjlem4 11640  adjbdln 11653  hartogOLD 15384  fisup2g 15768

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-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

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-clab 1872  df-cleq 1877  df-clel 1880  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-un 2600  df-sn 3049  df-pr 3050  df-uni 3178

Copyright terms: Public domain