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