Metamath Proof Explorer

Theorem reu2

Description: A way to express restricted uniqueness. (Contributed by NM, 22-Nov-1994)

Ref Expression
Assertion reu2 ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
2 1 eu2 ⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ∀ 𝑥 ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → 𝑥 = 𝑦 ) ) )
3 df-reu ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
4 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
5 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
6 19.21v ⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ) )
7 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
8 nfs1v ⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
9 7 8 nfan ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 )
10 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
11 sbequ12 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
12 10 11 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
13 9 12 sbiev ⊢ ( [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
14 13 anbi2i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
15 an4 ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
16 14 15 bitri ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
17 16 imbi1i ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) → 𝑥 = 𝑦 ) )
18 impexp ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
19 impexp ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ) )
20 17 18 19 3bitri ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ) )
21 20 albii ⊢ ( ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ) )
22 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
23 22 imbi2i ⊢ ( ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ) )
24 6 21 23 3bitr4i ⊢ ( ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
25 24 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
26 5 25 bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → 𝑥 = 𝑦 ) )
27 4 26 anbi12i ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ∀ 𝑥 ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → 𝑥 = 𝑦 ) ) )
28 2 3 27 3bitr4i ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )