This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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