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 
|- ( ( ph /\ x e. B ) -> -. ps )
Assertion rmounid 
|- ( ph -> ( E* x e. ( A u. B ) ps <-> E* x e. A ps ) )

Proof

Step Hyp Ref Expression
1 rmounid.1 
 |-  ( ( ph /\ x e. B ) -> -. ps )
2 1 ex 
 |-  ( ph -> ( x e. B -> -. ps ) )
3 2 con2d 
 |-  ( ph -> ( ps -> -. x e. B ) )
4 3 imp 
 |-  ( ( ph /\ ps ) -> -. x e. B )
5 biorf 
 |-  ( -. x e. B -> ( x e. A <-> ( x e. B \/ x e. A ) ) )
6 orcom 
 |-  ( ( x e. A \/ x e. B ) <-> ( x e. B \/ x e. A ) )
7 5 6 bitr4di 
 |-  ( -. x e. B -> ( x e. A <-> ( x e. A \/ x e. B ) ) )
8 4 7 syl 
 |-  ( ( ph /\ ps ) -> ( x e. A <-> ( x e. A \/ x e. B ) ) )
9 elun 
 |-  ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
10 8 9 bitr4di 
 |-  ( ( ph /\ ps ) -> ( x e. A <-> x e. ( A u. B ) ) )
11 10 pm5.32da 
 |-  ( ph -> ( ( ps /\ x e. A ) <-> ( ps /\ x e. ( A u. B ) ) ) )
12 11 biancomd 
 |-  ( ph -> ( ( ps /\ x e. A ) <-> ( x e. ( A u. B ) /\ ps ) ) )
13 12 bicomd 
 |-  ( ph -> ( ( x e. ( A u. B ) /\ ps ) <-> ( ps /\ x e. A ) ) )
14 13 biancomd 
 |-  ( ph -> ( ( x e. ( A u. B ) /\ ps ) <-> ( x e. A /\ ps ) ) )
15 14 mobidv 
 |-  ( ph -> ( E* x ( x e. ( A u. B ) /\ ps ) <-> E* x ( x e. A /\ ps ) ) )
16 df-rmo 
 |-  ( E* x e. ( A u. B ) ps <-> E* x ( x e. ( A u. B ) /\ ps ) )
17 df-rmo 
 |-  ( E* x e. A ps <-> E* x ( x e. A /\ ps ) )
18 15 16 17 3bitr4g 
 |-  ( ph -> ( E* x e. ( A u. B ) ps <-> E* x e. A ps ) )