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 ( ∃* 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝜑 → ( ∃* 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐵 𝜑 ) )

Proof

Step Hyp Ref Expression
1 mooran2 ⊢ ( ∃* 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) → ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
2 df-rmo ⊢ ( ∃* 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝜑 ) )
3 elun ⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
4 3 anbi1i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ 𝜑 ) )
5 andir ⊢ ( ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
6 4 5 bitri ⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
7 6 mobii ⊢ ( ∃* 𝑥 ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝜑 ) ↔ ∃* 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
8 2 7 bitri ⊢ ( ∃* 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝜑 ↔ ∃* 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
9 df-rmo ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
10 df-rmo ⊢ ( ∃* 𝑥 ∈ 𝐵 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) )
11 9 10 anbi12i ⊢ ( ( ∃* 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐵 𝜑 ) ↔ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
12 1 8 11 3imtr4i ⊢ ( ∃* 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝜑 → ( ∃* 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐵 𝜑 ) )