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

Proof

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