Metamath Proof Explorer

Theorem rmo3

Description: Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012) (Revised by NM, 16-Jun-2017) Avoid ax-13 . (Revised by Wolf Lammen, 30-Apr-2023)

Ref Expression
Hypothesis rmo2.1 ⊢ Ⅎ 𝑦 𝜑
Assertion rmo3 ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )

Proof

Step Hyp Ref Expression
1 rmo2.1 ⊢ Ⅎ 𝑦 𝜑
2 df-rmo ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
3 sban ⊢ ( [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( [ 𝑦 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
4 clelsb1 ⊢ ( [ 𝑦 / 𝑥 ] 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 )
5 4 anbi1i ⊢ ( ( [ 𝑦 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
6 3 5 bitri ⊢ ( [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
7 6 anbi2i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
8 an4 ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
9 ancom ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) )
10 9 anbi1i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
11 7 8 10 3bitri ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
12 11 imbi1i ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) → 𝑥 = 𝑦 ) )
13 impexp ⊢ ( ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
14 impexp ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ↔ ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ) )
15 12 13 14 3bitri ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ) )
16 15 albii ⊢ ( ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ) )
17 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ) )
18 r19.21v ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
19 16 17 18 3bitr2i ⊢ ( ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
20 19 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
21 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
22 21 1 nfan ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
23 22 mo3 ⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → 𝑥 = 𝑦 ) )
24 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
25 20 23 24 3bitr4i ⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
26 2 25 bitri ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )