Metamath Proof Explorer

Theorem reu8

Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 24-Oct-2006)

Ref Expression
Hypothesis rmo4.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion reu8 ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 rmo4.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2 1 cbvreuvw ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑦 ∈ 𝐴 𝜓 )
3 reu6 ⊢ ( ∃! 𝑦 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝜓 ↔ 𝑦 = 𝑥 ) )
4 dfbi2 ⊢ ( ( 𝜓 ↔ 𝑦 = 𝑥 ) ↔ ( ( 𝜓 → 𝑦 = 𝑥 ) ∧ ( 𝑦 = 𝑥 → 𝜓 ) ) )
5 4 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝜓 ↔ 𝑦 = 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ( ( 𝜓 → 𝑦 = 𝑥 ) ∧ ( 𝑦 = 𝑥 → 𝜓 ) ) )
6 ancom ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ∧ 𝜑 ) )
7 equcom ⊢ ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 )
8 7 imbi2i ⊢ ( ( 𝜓 → 𝑥 = 𝑦 ) ↔ ( 𝜓 → 𝑦 = 𝑥 ) )
9 8 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑦 = 𝑥 ) )
10 9 a1i ⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑦 = 𝑥 ) ) )
11 biimt ⊢ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ ( 𝑥 ∈ 𝐴 → 𝜑 ) ) )
12 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 = 𝑥 → 𝜓 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( 𝑦 = 𝑥 → 𝜓 ) ) )
13 bi2.04 ⊢ ( ( 𝑦 ∈ 𝐴 → ( 𝑦 = 𝑥 → 𝜓 ) ) ↔ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐴 → 𝜓 ) ) )
14 13 albii ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( 𝑦 = 𝑥 → 𝜓 ) ) ↔ ∀ 𝑦 ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐴 → 𝜓 ) ) )
15 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
16 15 1 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 → 𝜓 ) ) )
17 16 bicomd ⊢ ( 𝑥 = 𝑦 → ( ( 𝑦 ∈ 𝐴 → 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 → 𝜑 ) ) )
18 17 equcoms ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ 𝐴 → 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 → 𝜑 ) ) )
19 18 equsalvw ⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐴 → 𝜓 ) ) ↔ ( 𝑥 ∈ 𝐴 → 𝜑 ) )
20 12 14 19 3bitrri ⊢ ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 = 𝑥 → 𝜓 ) )
21 11 20 syl6bb ⊢ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 = 𝑥 → 𝜓 ) ) )
22 10 21 anbi12d ⊢ ( 𝑥 ∈ 𝐴 → ( ( ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ∧ 𝜑 ) ↔ ( ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑦 = 𝑥 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 = 𝑥 → 𝜓 ) ) ) )
23 6 22 syl5bb ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑦 = 𝑥 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 = 𝑥 → 𝜓 ) ) ) )
24 r19.26 ⊢ ( ∀ 𝑦 ∈ 𝐴 ( ( 𝜓 → 𝑦 = 𝑥 ) ∧ ( 𝑦 = 𝑥 → 𝜓 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑦 = 𝑥 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 = 𝑥 → 𝜓 ) ) )
25 23 24 syl6rbbr ⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( ( 𝜓 → 𝑦 = 𝑥 ) ∧ ( 𝑦 = 𝑥 → 𝜓 ) ) ↔ ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) ) )
26 5 25 syl5bb ⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( 𝜓 ↔ 𝑦 = 𝑥 ) ↔ ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) ) )
27 26 rexbiia ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝜓 ↔ 𝑦 = 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
28 2 3 27 3bitri ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )