Metamath Proof Explorer

Theorem rmoanim

Description: Introduction of a conjunct into restricted "at most one" quantifier, analogous to moanim . (Contributed by Alexander van der Vekens, 25-Jun-2017) Avoid ax-10 and ax-11 . (Revised by Gino Giotto, 24-Aug-2023)

Ref Expression
Hypothesis rmoanim.1 ⊢ Ⅎ 𝑥 𝜑
Assertion rmoanim ( ∃* 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step Hyp Ref Expression
1 rmoanim.1 ⊢ Ⅎ 𝑥 𝜑
2 impexp ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ↔ ( 𝜑 → ( 𝜓 → 𝑥 = 𝑦 ) ) )
3 2 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → ( 𝜓 → 𝑥 = 𝑦 ) ) )
4 1 r19.21 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → ( 𝜓 → 𝑥 = 𝑦 ) ) ↔ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
5 3 4 bitri ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ↔ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
6 5 exbii ⊢ ( ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ↔ ∃ 𝑦 ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
7 df-rmo ⊢ ( ∃* 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝜓 ) ) )
8 df-mo ⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝜓 ) ) ↔ ∃ 𝑦 ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝜓 ) ) → 𝑥 = 𝑦 ) )
9 impexp ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝜓 ) ) → 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )
10 9 albii ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝜓 ) ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )
11 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )
12 10 11 bitr4i ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝜓 ) ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) )
13 12 exbii ⊢ ( ∃ 𝑦 ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝜓 ) ) → 𝑥 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) )
14 7 8 13 3bitri ⊢ ( ∃* 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) )
15 df-rmo ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜓 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
16 df-mo ⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ∃ 𝑦 ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝑦 ) )
17 impexp ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝑥 = 𝑦 ) ) )
18 17 albii ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝑥 = 𝑦 ) ) )
19 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝑥 = 𝑦 ) ) )
20 18 19 bitr4i ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) )
21 20 exbii ⊢ ( ∃ 𝑦 ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) )
22 15 16 21 3bitri ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) )
23 22 imbi2i ⊢ ( ( 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜓 ) ↔ ( 𝜑 → ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
24 19.37v ⊢ ( ∃ 𝑦 ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) ↔ ( 𝜑 → ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
25 23 24 bitr4i ⊢ ( ( 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜓 ) ↔ ∃ 𝑦 ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
26 6 14 25 3bitr4i ⊢ ( ∃* 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜓 ) )