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