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 clelsb1fw ( [ 𝑦 / 𝑥 ] 𝑥𝐴𝑦𝐴 )
7 5 6 bianbi ( [ 𝑦 / 𝑥 ] ( 𝑥𝐴𝜑 ) ↔ ( 𝑦𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
8 7 anbi2i ( ( ( 𝑥𝐴𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥𝐴𝜑 ) ) ↔ ( ( 𝑥𝐴𝜑 ) ∧ ( 𝑦𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
9 an4 ( ( ( 𝑥𝐴𝜑 ) ∧ ( 𝑦𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) ↔ ( ( 𝑥𝐴𝑦𝐴 ) ∧ ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
10 ancom ( ( 𝑥𝐴𝑦𝐴 ) ↔ ( 𝑦𝐴𝑥𝐴 ) )
11 10 anbi1i ( ( ( 𝑥𝐴𝑦𝐴 ) ∧ ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) ↔ ( ( 𝑦𝐴𝑥𝐴 ) ∧ ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
12 8 9 11 3bitri ( ( ( 𝑥𝐴𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥𝐴𝜑 ) ) ↔ ( ( 𝑦𝐴𝑥𝐴 ) ∧ ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
13 12 imbi1i ( ( ( ( 𝑥𝐴𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥𝐴𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ( ( ( 𝑦𝐴𝑥𝐴 ) ∧ ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) → 𝑥 = 𝑦 ) )
14 impexp ( ( ( ( 𝑦𝐴𝑥𝐴 ) ∧ ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ( ( 𝑦𝐴𝑥𝐴 ) → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
15 impexp ( ( ( 𝑦𝐴𝑥𝐴 ) → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ↔ ( 𝑦𝐴 → ( 𝑥𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ) )
16 13 14 15 3bitri ( ( ( ( 𝑥𝐴𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥𝐴𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ( 𝑦𝐴 → ( 𝑥𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ) )
17 16 albii ( ∀ 𝑦 ( ( ( 𝑥𝐴𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥𝐴𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ( 𝑦𝐴 → ( 𝑥𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ) )
18 df-ral ( ∀ 𝑦𝐴 ( 𝑥𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ↔ ∀ 𝑦 ( 𝑦𝐴 → ( 𝑥𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ) )
19 2 nfcri 𝑦 𝑥𝐴
20 19 r19.21 ( ∀ 𝑦𝐴 ( 𝑥𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ↔ ( 𝑥𝐴 → ∀ 𝑦𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
21 17 18 20 3bitr2i ( ∀ 𝑦 ( ( ( 𝑥𝐴𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥𝐴𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ( 𝑥𝐴 → ∀ 𝑦𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
22 21 albii ( ∀ 𝑥𝑦 ( ( ( 𝑥𝐴𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥𝐴𝜑 ) ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥𝐴 → ∀ 𝑦𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
23 19 3 nfan 𝑦 ( 𝑥𝐴𝜑 )
24 23 mo3 ( ∃* 𝑥 ( 𝑥𝐴𝜑 ) ↔ ∀ 𝑥𝑦 ( ( ( 𝑥𝐴𝜑 ) ∧ [ 𝑦 / 𝑥 ] ( 𝑥𝐴𝜑 ) ) → 𝑥 = 𝑦 ) )
25 df-ral ( ∀ 𝑥𝐴𝑦𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥𝐴 → ∀ 𝑦𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
26 22 24 25 3bitr4i ( ∃* 𝑥 ( 𝑥𝐴𝜑 ) ↔ ∀ 𝑥𝐴𝑦𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
27 4 26 bitri ( ∃* 𝑥𝐴 𝜑 ↔ ∀ 𝑥𝐴𝑦𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )