This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rmoun

Description: "At most one" restricted existential quantifier for a union implies the same quantifier on both sets. (Contributed by Thierry Arnoux, 27-Nov-2023)

Ref Expression
Assertion rmoun ⊢ ∃* x ∈ A ∪ B φ → ∃* x ∈ A φ ∧ ∃* x ∈ B φ

Proof

Step Hyp Ref Expression
1 mooran2 ⊢ ∃* x x ∈ A ∧ φ ∨ x ∈ B ∧ φ → ∃* x x ∈ A ∧ φ ∧ ∃* x x ∈ B ∧ φ
2 df-rmo ⊢ ∃* x ∈ A ∪ B φ ↔ ∃* x x ∈ A ∪ B ∧ φ
3 elun ⊢ x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B
4 3 anbi1i ⊢ x ∈ A ∪ B ∧ φ ↔ x ∈ A ∨ x ∈ B ∧ φ
5 andir ⊢ x ∈ A ∨ x ∈ B ∧ φ ↔ x ∈ A ∧ φ ∨ x ∈ B ∧ φ
6 4 5 bitri ⊢ x ∈ A ∪ B ∧ φ ↔ x ∈ A ∧ φ ∨ x ∈ B ∧ φ
7 6 mobii ⊢ ∃* x x ∈ A ∪ B ∧ φ ↔ ∃* x x ∈ A ∧ φ ∨ x ∈ B ∧ φ
8 2 7 bitri ⊢ ∃* x ∈ A ∪ B φ ↔ ∃* x x ∈ A ∧ φ ∨ x ∈ B ∧ φ
9 df-rmo ⊢ ∃* x ∈ A φ ↔ ∃* x x ∈ A ∧ φ
10 df-rmo ⊢ ∃* x ∈ B φ ↔ ∃* x x ∈ B ∧ φ
11 9 10 anbi12i ⊢ ∃* x ∈ A φ ∧ ∃* x ∈ B φ ↔ ∃* x x ∈ A ∧ φ ∧ ∃* x x ∈ B ∧ φ
12 1 8 11 3imtr4i ⊢ ∃* x ∈ A ∪ B φ → ∃* x ∈ A φ ∧ ∃* x ∈ B φ