Theorem reu3 1927

Description: A way to express restricted uniqueness.

Assertion

Ref	Expression
reu3	⊢ (∃!x ∈ A φ ↔ ∃y ∈ A ∀x ∈ A (φ ↔ x = y))

Distinct variable groups:   x,y,A   φ,y

Proof of Theorem reu3

Step	Hyp	Ref	Expression
1		df-reu 1648	. 2 ⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ⋀ φ))
2		df-eu 1380	. 2 ⊢ (∃!x(x ∈ A ⋀ φ) ↔ ∃y∀x((x ∈ A ⋀ φ) ↔ x = y))
3		19.28v 1297	. . . . 5 ⊢ (∀x(y ∈ A ⋀ (x ∈ A → (φ ↔ x = y))) ↔ (y ∈ A ⋀ ∀x(x ∈ A → (φ ↔ x = y))))
4		eleq1 1531	. . . . . . . . . . . 12 ⊢ (x = y → (x ∈ A ↔ y ∈ A))
5		sbequ12 1179	. . . . . . . . . . . 12 ⊢ (x = y → (φ ↔ [y / x]φ))
6	4, 5	anbi12d 627	. . . . . . . . . . 11 ⊢ (x = y → ((x ∈ A ⋀ φ) ↔ (y ∈ A ⋀ [y / x]φ)))
7		eqeq1 1478	. . . . . . . . . . 11 ⊢ (x = y → (x = y ↔ y = y))
8	6, 7	bibi12d 628	. . . . . . . . . 10 ⊢ (x = y → (((x ∈ A ⋀ φ) ↔ x = y) ↔ ((y ∈ A ⋀ [y / x]φ) ↔ y = y)))
9		eqid 1473	. . . . . . . . . . . 12 ⊢ y = y
10	9	tbt 719	. . . . . . . . . . 11 ⊢ ((y ∈ A ⋀ [y / x]φ) ↔ ((y ∈ A ⋀ [y / x]φ) ↔ y = y))
11		pm3.26 319	. . . . . . . . . . 11 ⊢ ((y ∈ A ⋀ [y / x]φ) → y ∈ A)
12	10, 11	sylbir 201	. . . . . . . . . 10 ⊢ (((y ∈ A ⋀ [y / x]φ) ↔ y = y) → y ∈ A)
13	8, 12	syl6bi 214	. . . . . . . . 9 ⊢ (x = y → (((x ∈ A ⋀ φ) ↔ x = y) → y ∈ A))
14	13	a4imv 1205	. . . . . . . 8 ⊢ (∀x((x ∈ A ⋀ φ) ↔ x = y) → y ∈ A)
15		bi1 148	. . . . . . . . . . . . 13 ⊢ (((x ∈ A ⋀ φ) ↔ x = y) → ((x ∈ A ⋀ φ) → x = y))
16	15	exp3a 375	. . . . . . . . . . . 12 ⊢ (((x ∈ A ⋀ φ) ↔ x = y) → (x ∈ A → (φ → x = y)))
17	16	imp 350	. . . . . . . . . . 11 ⊢ ((((x ∈ A ⋀ φ) ↔ x = y) ⋀ x ∈ A) → (φ → x = y))
18		bi2 149	. . . . . . . . . . . . 13 ⊢ (((x ∈ A ⋀ φ) ↔ x = y) → (x = y → (x ∈ A ⋀ φ)))
19		pm3.27 323	. . . . . . . . . . . . 13 ⊢ ((x ∈ A ⋀ φ) → φ)
20	18, 19	syl6 22	. . . . . . . . . . . 12 ⊢ (((x ∈ A ⋀ φ) ↔ x = y) → (x = y → φ))
21	20	adantr 389	. . . . . . . . . . 11 ⊢ ((((x ∈ A ⋀ φ) ↔ x = y) ⋀ x ∈ A) → (x = y → φ))
22	17, 21	impbid 515	. . . . . . . . . 10 ⊢ ((((x ∈ A ⋀ φ) ↔ x = y) ⋀ x ∈ A) → (φ ↔ x = y))
23	22	ex 373	. . . . . . . . 9 ⊢ (((x ∈ A ⋀ φ) ↔ x = y) → (x ∈ A → (φ ↔ x = y)))
24	23	a4s 982	. . . . . . . 8 ⊢ (∀x((x ∈ A ⋀ φ) ↔ x = y) → (x ∈ A → (φ ↔ x = y)))
25	14, 24	jca 288	. . . . . . 7 ⊢ (∀x((x ∈ A ⋀ φ) ↔ x = y) → (y ∈ A ⋀ (x ∈ A → (φ ↔ x = y))))
26	25	a5i 987	. . . . . 6 ⊢ (∀x((x ∈ A ⋀ φ) ↔ x = y) → ∀x(y ∈ A ⋀ (x ∈ A → (φ ↔ x = y))))
27		bi1 148	. . . . . . . . . . 11 ⊢ ((φ ↔ x = y) → (φ → x = y))
28	27	imim2i 17	. . . . . . . . . 10 ⊢ ((x ∈ A → (φ ↔ x = y)) → (x ∈ A → (φ → x = y)))
29	28	imp3a 361	. . . . . . . . 9 ⊢ ((x ∈ A → (φ ↔ x = y)) → ((x ∈ A ⋀ φ) → x = y))
30	29	adantl 388	. . . . . . . 8 ⊢ ((y ∈ A ⋀ (x ∈ A → (φ ↔ x = y))) → ((x ∈ A ⋀ φ) → x = y))
31		eleq1a 1540	. . . . . . . . . . . 12 ⊢ (y ∈ A → (x = y → x ∈ A))
32	31	adantr 389	. . . . . . . . . . 11 ⊢ ((y ∈ A ⋀ (x ∈ A → (φ ↔ x = y))) → (x = y → x ∈ A))
33	32	imp 350	. . . . . . . . . 10 ⊢ (((y ∈ A ⋀ (x ∈ A → (φ ↔ x = y))) ⋀ x = y) → x ∈ A)
34		bi2 149	. . . . . . . . . . . . . 14 ⊢ ((φ ↔ x = y) → (x = y → φ))
35	34	imim2i 17	. . . . . . . . . . . . 13 ⊢ ((x ∈ A → (φ ↔ x = y)) → (x ∈ A → (x = y → φ)))
36	35	com23 32	. . . . . . . . . . . 12 ⊢ ((x ∈ A → (φ ↔ x = y)) → (x = y → (x ∈ A → φ)))
37	36	imp 350	. . . . . . . . . . 11 ⊢ (((x ∈ A → (φ ↔ x = y)) ⋀ x = y) → (x ∈ A → φ))
38	37	adantll 392	. . . . . . . . . 10 ⊢ (((y ∈ A ⋀ (x ∈ A → (φ ↔ x = y))) ⋀ x = y) → (x ∈ A → φ))
39	33, 38	jcai 289	. . . . . . . . 9 ⊢ (((y ∈ A ⋀ (x ∈ A → (φ ↔ x = y))) ⋀ x = y) → (x ∈ A ⋀ φ))
40	39	ex 373	. . . . . . . 8 ⊢ ((y ∈ A ⋀ (x ∈ A → (φ ↔ x = y))) → (x = y → (x ∈ A ⋀ φ)))
41	30, 40	impbid 515	. . . . . . 7 ⊢ ((y ∈ A ⋀ (x ∈ A → (φ ↔ x = y))) → ((x ∈ A ⋀ φ) ↔ x = y))
42	41	19.20i 990	. . . . . 6 ⊢ (∀x(y ∈ A ⋀ (x ∈ A → (φ ↔ x = y))) → ∀x((x ∈ A ⋀ φ) ↔ x = y))
43	26, 42	impbi 157	. . . . 5 ⊢ (∀x((x ∈ A ⋀ φ) ↔ x = y) ↔ ∀x(y ∈ A ⋀ (x ∈ A → (φ ↔ x = y))))
44		df-ral 1646	. . . . . 6 ⊢ (∀x ∈ A (φ ↔ x = y) ↔ ∀x(x ∈ A → (φ ↔ x = y)))
45	44	anbi2i 480	. . . . 5 ⊢ ((y ∈ A ⋀ ∀x ∈ A (φ ↔ x = y)) ↔ (y ∈ A ⋀ ∀x(x ∈ A → (φ ↔ x = y))))
46	3, 43, 45	3bitr4 183	. . . 4 ⊢ (∀x((x ∈ A ⋀ φ) ↔ x = y) ↔ (y ∈ A ⋀ ∀x ∈ A (φ ↔ x = y)))
47	46	exbii 1049	. . 3 ⊢ (∃y∀x((x ∈ A ⋀ φ) ↔ x = y) ↔ ∃y(y ∈ A ⋀ ∀x ∈ A (φ ↔ x = y)))
48		df-rex 1647	. . 3 ⊢ (∃y ∈ A ∀x ∈ A (φ ↔ x = y) ↔ ∃y(y ∈ A ⋀ ∀x ∈ A (φ ↔ x = y)))
49	47, 48	bitr4 176	. 2 ⊢ (∃y∀x((x ∈ A ⋀ φ) ↔ x = y) ↔ ∃y ∈ A ∀x ∈ A (φ ↔ x = y))
50	1, 2, 49	3bitr 177	1 ⊢ (∃!x ∈ A φ ↔ ∃y ∈ A ∀x ∈ A (φ ↔ x = y))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978  [wsbc 1168  ∃!weu 1378  ∀wral 1642  ∃wrex 1643  ∃!wreu 1644

This theorem is referenced by:  reu6 1928  reu8 1932

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-9o 1121  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-cleq 1467  df-clel 1470  df-ral 1646  df-rex 1647  df-reu 1648

Copyright terms: Public domain