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 φ x B ¬ ψ
Assertion rmounid φ * x A B ψ * x A ψ

Proof

Step Hyp Ref Expression
1 rmounid.1 φ x B ¬ ψ
2 1 ex φ x B ¬ ψ
3 2 con2d φ ψ ¬ x B
4 3 imp φ ψ ¬ x B
5 biorf ¬ x B x A x B x A
6 orcom x A x B x B x A
7 5 6 bitr4di ¬ x B x A x A x B
8 4 7 syl φ ψ x A x A x B
9 elun x A B x A x B
10 8 9 bitr4di φ ψ x A x A B
11 10 pm5.32da φ ψ x A ψ x A B
12 11 biancomd φ ψ x A x A B ψ
13 12 bicomd φ x A B ψ ψ x A
14 13 biancomd φ x A B ψ x A ψ
15 14 mobidv φ * x x A B ψ * x x A ψ
16 df-rmo * x A B ψ * x x A B ψ
17 df-rmo * x A ψ * x x A ψ
18 15 16 17 3bitr4g φ * x A B ψ * x A ψ