Theorem reu3 3693

Description: A way to express restricted uniqueness. (Contributed by NM, 24-Oct-2006.)

Assertion

Ref	Expression
reu3	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)))

Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem reu3

Step	Hyp	Ref	Expression
1		reurex 3374	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑)
2		reu6 3692	. . . 4 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦))
3		biimp 218	. . . . . 6 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝜑 → 𝑥 = 𝑦))
4	3	ralimi 3102	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦))
5	4	reximi 3103	. . . 4 ⊢ (∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦) → ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦))
6	2, 5	sylbi 220	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦))
7	1, 6	jca 520	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)))
8		rexex 3095	. . . 4 ⊢ (∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦) → ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦))
9	8	anim2i 628	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) → (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)))
10		eu3v 2600	. . . 4 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦)))
11		df-reu 3371	. . . 4 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
12		df-rex 3090	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
13		df-ral 3080	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝑥 = 𝑦)))
14		impexp 455	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 → (𝜑 → 𝑥 = 𝑦)))
15	14	albii 1842	. . . . . . 7 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝑥 = 𝑦)))
16	13, 15	bitr4i 281	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦) ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦))
17	16	exbii 1871	. . . . 5 ⊢ (∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦) ↔ ∃𝑦∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦))
18	12, 17	anbi12i 639	. . . 4 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦)))
19	10, 11, 18	3bitr4i 306	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)))
20	9, 19	sylibr 237	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) → ∃!𝑥 ∈ 𝐴 𝜑)
21	7, 20	impbii 212	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1561  ∃wex 1802   ∈ wcel 2145  ∃!weu 2598  ∀wral 3079  ∃wrex 3089  ∃!wreu 3368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-10 2178  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clel 2840  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371

This theorem is referenced by:  reu7  3698  2reu4lem  4480  reu3op  6283