Metamath Proof Explorer

Theorem rmo3f

Description: Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012) (Revised by NM, 16-Jun-2017) (Revised by Thierry Arnoux, 8-Oct-2017)

Ref Expression
Hypotheses rmo3f.1 ⊢ Ⅎ 𝑥 𝐴
rmo3f.2 ⊢ Ⅎ 𝑦 𝐴
rmo3f.3 ⊢ Ⅎ 𝑦 𝜑
Assertion rmo3f ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )

Proof

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