This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) )