Theorem reu6

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

	Ref	Expression
Assertion	reu6	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		df-reu	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
2		19.28v	⊢ ( ∀ 𝑥 ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) )
3		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
4		sbequ12	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
5	3 4	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
6		equequ1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑦 ) )
7	5 6	bibi12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ 𝑦 = 𝑦 ) ) )
8		equid	⊢ 𝑦 = 𝑦
9	8	tbt	⊢ ( ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ 𝑦 = 𝑦 ) )
10		simpl	⊢ ( ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑦 ∈ 𝐴 )
11	9 10	sylbir	⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ 𝑦 = 𝑦 ) → 𝑦 ∈ 𝐴 )
12	7 11	biimtrdi	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) → 𝑦 ∈ 𝐴 ) )
13	12	spimvw	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) → 𝑦 ∈ 𝐴 )
14		ibar	⊢ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
15	14	bibi1d	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) ) )
16	15	biimprcd	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
17	16	sps	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
18	13 17	jca	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) → ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) )
19	18	axc4i	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) → ∀ 𝑥 ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) )
20		biimp	⊢ ( ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( 𝜑 → 𝑥 = 𝑦 ) )
21	20	imim2i	⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) → ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝑥 = 𝑦 ) ) )
22	21	impd	⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) )
23	22	adantl	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) )
24	3	biimprcd	⊢ ( 𝑦 ∈ 𝐴 → ( 𝑥 = 𝑦 → 𝑥 ∈ 𝐴 ) )
25	24	adantr	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) → ( 𝑥 = 𝑦 → 𝑥 ∈ 𝐴 ) )
26	25	imp	⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → 𝑥 ∈ 𝐴 )
27		simplr	⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
28		simpr	⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝑦 )
29		biimpr	⊢ ( ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( 𝑥 = 𝑦 → 𝜑 ) )
30	27 28 29	syl6ci	⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
31	26 30	jcai	⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
32	31	ex	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) → ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
33	23 32	impbid	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) )
34	33	alimi	⊢ ( ∀ 𝑥 ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) )
35	19 34	impbii	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) )
36		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
37	36	anbi2i	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) )
38	2 35 37	3bitr4i	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
39	38	exbii	⊢ ( ∃ 𝑦 ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
40		eu6	⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑦 ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) )
41		df-rex	⊢ ( ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
42	39 40 41	3bitr4i	⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
43	1 42	bitri	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) )