Metamath Proof Explorer

Theorem rmo4

Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006) (Revised by NM, 16-Jun-2017)

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

Proof

Step Hyp Ref Expression
1 rmo4.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2 df-rmo ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
3 an4 ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝜑 ∧ 𝜓 ) ) )
4 ancom ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) )
5 4 anbi1i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝜑 ∧ 𝜓 ) ) )
6 3 5 bitri ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝜑 ∧ 𝜓 ) ) )
7 6 imbi1i ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) → 𝑥 = 𝑦 ) ↔ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → 𝑥 = 𝑦 ) )
8 impexp ⊢ ( ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → 𝑥 = 𝑦 ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )
9 impexp ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ↔ ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ) )
10 7 8 9 3bitri ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) → 𝑥 = 𝑦 ) ↔ ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ) )
11 10 albii ⊢ ( ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ) )
12 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ) )
13 r19.21v ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )
14 11 12 13 3bitr2i ⊢ ( ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) → 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )
15 14 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )
16 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
17 16 1 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
18 17 mo4 ⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) → 𝑥 = 𝑦 ) )
19 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )
20 15 18 19 3bitr4i ⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) )
21 2 20 bitri ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) )