Theorem reucl 2891

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

Assertion

Ref	Expression
reucl	⊢ (∃!x ∈ A φ → ∪{x ∈ A∣φ} ∈ A)

Distinct variable group:   x,A

Proof of Theorem reucl

Step	Hyp	Ref	Expression
1		eusn 2450	. . 3 ⊢ (∃!x(x ∈ A ⋀ φ) ↔ ∃x{x∣(x ∈ A ⋀ φ)} = {x})
2		hbab1 1469	. . . . . 6 ⊢ (y ∈ {x∣(x ∈ A ⋀ φ)} → ∀x y ∈ {x∣(x ∈ A ⋀ φ)})
3	2	hbuni 2513	. . . . 5 ⊢ (y ∈ ∪{x∣(x ∈ A ⋀ φ)} → ∀x y ∈ ∪{x∣(x ∈ A ⋀ φ)})
4		ax-17 973	. . . . 5 ⊢ (y ∈ A → ∀x y ∈ A)
5	3, 4	hbel 1569	. . . 4 ⊢ (∪{x∣(x ∈ A ⋀ φ)} ∈ A → ∀x∪{x∣(x ∈ A ⋀ φ)} ∈ A)
6		unieq 2514	. . . . . 6 ⊢ ({x∣(x ∈ A ⋀ φ)} = {x} → ∪{x∣(x ∈ A ⋀ φ)} = ∪{x})
7		visset 1816	. . . . . . 7 ⊢ x ∈ V
8	7	unisn 2521	. . . . . 6 ⊢ ∪{x} = x
9	6, 8	syl6req 1527	. . . . 5 ⊢ ({x∣(x ∈ A ⋀ φ)} = {x} → x = ∪{x∣(x ∈ A ⋀ φ)})
10	7	snid 2439	. . . . . . . 8 ⊢ x ∈ {x}
11		eleq2 1538	. . . . . . . 8 ⊢ ({x∣(x ∈ A ⋀ φ)} = {x} → (x ∈ {x∣(x ∈ A ⋀ φ)} ↔ x ∈ {x}))
12	10, 11	mpbiri 194	. . . . . . 7 ⊢ ({x∣(x ∈ A ⋀ φ)} = {x} → x ∈ {x∣(x ∈ A ⋀ φ)})
13		abid 1468	. . . . . . 7 ⊢ (x ∈ {x∣(x ∈ A ⋀ φ)} ↔ (x ∈ A ⋀ φ))
14	12, 13	sylib 198	. . . . . 6 ⊢ ({x∣(x ∈ A ⋀ φ)} = {x} → (x ∈ A ⋀ φ))
15	14	pm3.26d 321	. . . . 5 ⊢ ({x∣(x ∈ A ⋀ φ)} = {x} → x ∈ A)
16	9, 15	eqeltrrd 1552	. . . 4 ⊢ ({x∣(x ∈ A ⋀ φ)} = {x} → ∪{x∣(x ∈ A ⋀ φ)} ∈ A)
17	5, 16	19.23ai 1066	. . 3 ⊢ (∃x{x∣(x ∈ A ⋀ φ)} = {x} → ∪{x∣(x ∈ A ⋀ φ)} ∈ A)
18	1, 17	sylbi 199	. 2 ⊢ (∃!x(x ∈ A ⋀ φ) → ∪{x∣(x ∈ A ⋀ φ)} ∈ A)
19		df-reu 1654	. 2 ⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ⋀ φ))
20		df-rab 1655	. . . 4 ⊢ {x ∈ A∣φ} = {x∣(x ∈ A ⋀ φ)}
21	20	unieqi 2515	. . 3 ⊢ ∪{x ∈ A∣φ} = ∪{x∣(x ∈ A ⋀ φ)}
22	21	eleq1i 1540	. 2 ⊢ (∪{x ∈ A∣φ} ∈ A ↔ ∪{x∣(x ∈ A ⋀ φ)} ∈ A)
23	18, 19, 22	3imtr4 219	1 ⊢ (∃!x ∈ A φ → ∪{x ∈ A∣φ} ∈ A)

Syntax hints:   → wi 3   ⋀ wa 223   = wceq 958   ∈ wcel 960  ∃wex 982  ∃!weu 1382  {cab 1466  ∃!wreu 1650  {crab 1651  {csn 2413  ∪cuni 2507

This theorem is referenced by:  reuuni3 2892  reuuni4 2893  reucl2 2894  reuuniss 2895  reuuniss2 2897  reuunixfr 2912  wereucl 2952  supcl 4588  aceq6a 4751  subcl 5378  divcl 5722  uzwo3lem2 6219  flclt 6228  reclt 6758  imclt 6759  isumclt 7209  grpidcl 8055  grpinvcl 8064  minveccl 8580  spwcl 8656  axpjclt 9235  cnlnadjlem3 9997  cnlnadjlem4 9998  adjbdlnt 10011

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-clab 1467  df-cleq 1472  df-clel 1475  df-reu 1654  df-rab 1655  df-v 1815  df-un 2053  df-sn 2416  df-pr 2417  df-uni 2508

Copyright terms: Public domain