Theorem reucl 1957

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(s):   x,A

Proof of Theorem reucl

Step	Hyp	Ref	Expression
1		eusn 1913	. . 3 |- (E!x(x e. A /\ ph) <-> E.x{x | (x e. A /\ ph)} = {x})
2		hbab1 1095	. . . . . 6 |- (y e. {x | (x e. A /\ ph)} -> A.x y e. {x | (x e. A /\ ph)})
3	2	hbuni 1925	. . . . 5 |- (y e. U.{x | (x e. A /\ ph)} -> A.x y e. U.{x | (x e. A /\ ph)})
4		ax-17 925	. . . . 5 |- (y e. A -> A.x y e. A)
5	3, 4	hbel 1172	. . . 4 |- (U.{x | (x e. A /\ ph)} e. A -> A.xU.{x | (x e. A /\ ph)} e. A)
6		unieq 1927	. . . . . 6 |- ({x | (x e. A /\ ph)} = {x} -> U.{x | (x e. A /\ ph)} = U.{x})
7		visset 1350	. . . . . . 7 |- x e. V
8	7	unisn 1932	. . . . . 6 |- U.{x} = x
9	6, 8	syl6req 1141	. . . . 5 |- ({x | (x e. A /\ ph)} = {x} -> x = U.{x | (x e. A /\ ph)})
10	7	snid 1830	. . . . . . . 8 |- x e. {x}
11		eleq2 1150	. . . . . . . 8 |- ({x | (x e. A /\ ph)} = {x} -> (x e. {x | (x e. A /\ ph)} <-> x e. {x}))
12	10, 11	mpbiri 169	. . . . . . 7 |- ({x | (x e. A /\ ph)} = {x} -> x e. {x | (x e. A /\ ph)})
13		abid 1094	. . . . . . 7 |- (x e. {x | (x e. A /\ ph)} <-> (x e. A /\ ph))
14	12, 13	sylib 173	. . . . . 6 |- ({x | (x e. A /\ ph)} = {x} -> (x e. A /\ ph))
15	14	pm3.26d 258	. . . . 5 |- ({x | (x e. A /\ ph)} = {x} -> x e. A)
16	9, 15	eqeltrrd 1164	. . . 4 |- ({x | (x e. A /\ ph)} = {x} -> U.{x | (x e. A /\ ph)} e. A)
17	5, 16	19.23ai 746	. . 3 |- (E.x{x | (x e. A /\ ph)} = {x} -> U.{x | (x e. A /\ ph)} e. A)
18	1, 17	sylbi 174	. 2 |- (E!x(x e. A /\ ph) -> U.{x | (x e. A /\ ph)} e. A)
19		df-reu 1207	. 2 |- (E!x e. A ph <-> E!x(x e. A /\ ph))
20		df-rab 1208	. . . 4 |- {x e. A | ph} = {x | (x e. A /\ ph)}
21	20	unieqi 1928	. . 3 |- U.{x e. A | ph} = U.{x | (x e. A /\ ph)}
22	21	eleq1i 1152	. 2 |- (U.{x e. A | ph} e. A <-> U.{x | (x e. A /\ ph)} e. A)
23	18, 19, 22	3imtr4 192	1 |- (E!x e. A ph -> U.{x e. A | ph} e. A)

Syntax hints:   -> wi 2   /\ wa 196  E.wex 678  E!weu 1007  {cab 1090   = wceq 1091   e. wcel 1092  E!wreu 1203  {crab 1204  {csn 1808  U.cuni 1919

This theorem is referenced by:  reuuni3 1958  reuuni4 1959  supcl 2159  aceq6a 3564  zornlem1 3603  htalem 3618  subcl 4139  divcl 4221  uzwo3lem2 4615  flclt 4624  reclt 4796  imclt 4797  axpjclt 5247

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-clab 1093  df-cleq 1097  df-clel 1099  df-reu 1207  df-rab 1208  df-v 1349  df-un 1490  df-sn 1811  df-pr 1812  df-uni 1920

metamath.org