Theorem reucl 2880

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		eusn 2442	. . 3 |- (E!x(x e. A /\ ph) <-> E.x{x | (x e. A /\ ph)} = {x})
2		hbab1 1464	. . . . . 6 |- (y e. {x | (x e. A /\ ph)} -> A.x y e. {x | (x e. A /\ ph)})
3	2	hbuni 2504	. . . . 5 |- (y e. U.{x | (x e. A /\ ph)} -> A.x y e. U.{x | (x e. A /\ ph)})
4		ax-17 969	. . . . 5 |- (y e. A -> A.x y e. A)
5	3, 4	hbel 1563	. . . 4 |- (U.{x | (x e. A /\ ph)} e. A -> A.xU.{x | (x e. A /\ ph)} e. A)
6		unieq 2505	. . . . . 6 |- ({x | (x e. A /\ ph)} = {x} -> U.{x | (x e. A /\ ph)} = U.{x})
7		visset 1809	. . . . . . 7 |- x e. V
8	7	unisn 2512	. . . . . 6 |- U.{x} = x
9	6, 8	syl6req 1521	. . . . 5 |- ({x | (x e. A /\ ph)} = {x} -> x = U.{x | (x e. A /\ ph)})
10	7	snid 2431	. . . . . . . 8 |- x e. {x}
11		eleq2 1532	. . . . . . . 8 |- ({x | (x e. A /\ ph)} = {x} -> (x e. {x | (x e. A /\ ph)} <-> x e. {x}))
12	10, 11	mpbiri 194	. . . . . . 7 |- ({x | (x e. A /\ ph)} = {x} -> x e. {x | (x e. A /\ ph)})
13		abid 1463	. . . . . . 7 |- (x e. {x | (x e. A /\ ph)} <-> (x e. A /\ ph))
14	12, 13	sylib 198	. . . . . 6 |- ({x | (x e. A /\ ph)} = {x} -> (x e. A /\ ph))
15	14	pm3.26d 321	. . . . 5 |- ({x | (x e. A /\ ph)} = {x} -> x e. A)
16	9, 15	eqeltrrd 1546	. . . 4 |- ({x | (x e. A /\ ph)} = {x} -> U.{x | (x e. A /\ ph)} e. A)
17	5, 16	19.23ai 1062	. . 3 |- (E.x{x | (x e. A /\ ph)} = {x} -> U.{x | (x e. A /\ ph)} e. A)
18	1, 17	sylbi 199	. 2 |- (E!x(x e. A /\ ph) -> U.{x | (x e. A /\ ph)} e. A)
19		df-reu 1648	. 2 |- (E!x e. A ph <-> E!x(x e. A /\ ph))
20		df-rab 1649	. . . 4 |- {x e. A | ph} = {x | (x e. A /\ ph)}
21	20	unieqi 2506	. . 3 |- U.{x e. A | ph} = U.{x | (x e. A /\ ph)}
22	21	eleq1i 1534	. 2 |- (U.{x e. A | ph} e. A <-> U.{x | (x e. A /\ ph)} e. A)
23	18, 19, 22	3imtr4 219	1 |- (E!x e. A ph -> U.{x e. A | ph} e. A)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 954   e. wcel 956  E.wex 978  E!weu 1378  {cab 1461  E!wreu 1644  {crab 1645  {csn 2405  U.cuni 2498

This theorem is referenced by:  reuuni3 2881  reuuni4 2882  reucl2 2883  reuuniss 2884  reuuniss2 2886  reuunixfr 2901  wereucl 2941  supcl 4559  aceq6a 4721  subcl 5346  divcl 5687  uzwo3lem2 6173  flclt 6182  reclt 6696  imclt 6697  isumclt 7152  grpidcl 8009  grpinvcl 8018  minveccl 8528  spwcl 8601  axpjclt 9178  cnlnadjlem3 9940  cnlnadjlem4 9941  adjbdlnt 9954

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-10 964  ax-12 966  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

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-clab 1462  df-cleq 1467  df-clel 1470  df-reu 1648  df-rab 1649  df-v 1808  df-un 2046  df-sn 2408  df-pr 2409  df-uni 2499

Copyright terms: Public domain