Metamath Proof Explorer

Theorem rmounid

Description: A case where an "at most one" restricted existential quantifier for a union is equivalent to such a quantifier for one of the sets. (Contributed by Thierry Arnoux, 27-Nov-2023)

Ref Expression
Hypothesis rmounid.1 ⊢ φ ∧ x ∈ B → ¬ ψ
Assertion rmounid ⊢ φ → ∃* x ∈ A ∪ B ψ ↔ ∃* x ∈ A ψ

Proof

Step Hyp Ref Expression
1 rmounid.1 ⊢ φ ∧ x ∈ B → ¬ ψ
2 1 ex ⊢ φ → x ∈ B → ¬ ψ
3 2 con2d ⊢ φ → ψ → ¬ x ∈ B
4 3 imp ⊢ φ ∧ ψ → ¬ x ∈ B
5 biorf ⊢ ¬ x ∈ B → x ∈ A ↔ x ∈ B ∨ x ∈ A
6 orcom ⊢ x ∈ A ∨ x ∈ B ↔ x ∈ B ∨ x ∈ A
7 5 6 bitr4di ⊢ ¬ x ∈ B → x ∈ A ↔ x ∈ A ∨ x ∈ B
8 4 7 syl ⊢ φ ∧ ψ → x ∈ A ↔ x ∈ A ∨ x ∈ B
9 elun ⊢ x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B
10 8 9 bitr4di ⊢ φ ∧ ψ → x ∈ A ↔ x ∈ A ∪ B
11 10 pm5.32da ⊢ φ → ψ ∧ x ∈ A ↔ ψ ∧ x ∈ A ∪ B
12 11 biancomd ⊢ φ → ψ ∧ x ∈ A ↔ x ∈ A ∪ B ∧ ψ
13 12 bicomd ⊢ φ → x ∈ A ∪ B ∧ ψ ↔ ψ ∧ x ∈ A
14 13 biancomd ⊢ φ → x ∈ A ∪ B ∧ ψ ↔ x ∈ A ∧ ψ
15 14 mobidv ⊢ φ → ∃* x x ∈ A ∪ B ∧ ψ ↔ ∃* x x ∈ A ∧ ψ
16 df-rmo ⊢ ∃* x ∈ A ∪ B ψ ↔ ∃* x x ∈ A ∪ B ∧ ψ
17 df-rmo ⊢ ∃* x ∈ A ψ ↔ ∃* x x ∈ A ∧ ψ
18 15 16 17 3bitr4g ⊢ φ → ∃* x ∈ A ∪ B ψ ↔ ∃* x ∈ A ψ