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

Metamath Proof Explorer

Theorem rmoanim

Description: Introduction of a conjunct into restricted "at most one" quantifier, analogous to moanim . (Contributed by Alexander van der Vekens, 25-Jun-2017) Avoid ax-10 and ax-11 . (Revised by GG, 24-Aug-2023)

Ref Expression
Hypothesis rmoanim.1 
|- F/ x ph
Assertion rmoanim 
|- ( E* x e. A ( ph /\ ps ) <-> ( ph -> E* x e. A ps ) )

Proof

Step Hyp Ref Expression
1 rmoanim.1 
 |-  F/ x ph
2 impexp 
 |-  ( ( ( ph /\ ps ) -> x = y ) <-> ( ph -> ( ps -> x = y ) ) )
3 2 ralbii 
 |-  ( A. x e. A ( ( ph /\ ps ) -> x = y ) <-> A. x e. A ( ph -> ( ps -> x = y ) ) )
4 1 r19.21 
 |-  ( A. x e. A ( ph -> ( ps -> x = y ) ) <-> ( ph -> A. x e. A ( ps -> x = y ) ) )
5 3 4 bitri 
 |-  ( A. x e. A ( ( ph /\ ps ) -> x = y ) <-> ( ph -> A. x e. A ( ps -> x = y ) ) )
6 5 exbii 
 |-  ( E. y A. x e. A ( ( ph /\ ps ) -> x = y ) <-> E. y ( ph -> A. x e. A ( ps -> x = y ) ) )
7 df-rmo 
 |-  ( E* x e. A ( ph /\ ps ) <-> E* x ( x e. A /\ ( ph /\ ps ) ) )
8 df-mo 
 |-  ( E* x ( x e. A /\ ( ph /\ ps ) ) <-> E. y A. x ( ( x e. A /\ ( ph /\ ps ) ) -> x = y ) )
9 impexp 
 |-  ( ( ( x e. A /\ ( ph /\ ps ) ) -> x = y ) <-> ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) )
10 9 albii 
 |-  ( A. x ( ( x e. A /\ ( ph /\ ps ) ) -> x = y ) <-> A. x ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) )
11 df-ral 
 |-  ( A. x e. A ( ( ph /\ ps ) -> x = y ) <-> A. x ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) )
12 10 11 bitr4i 
 |-  ( A. x ( ( x e. A /\ ( ph /\ ps ) ) -> x = y ) <-> A. x e. A ( ( ph /\ ps ) -> x = y ) )
13 12 exbii 
 |-  ( E. y A. x ( ( x e. A /\ ( ph /\ ps ) ) -> x = y ) <-> E. y A. x e. A ( ( ph /\ ps ) -> x = y ) )
14 7 8 13 3bitri 
 |-  ( E* x e. A ( ph /\ ps ) <-> E. y A. x e. A ( ( ph /\ ps ) -> x = y ) )
15 df-rmo 
 |-  ( E* x e. A ps <-> E* x ( x e. A /\ ps ) )
16 df-mo 
 |-  ( E* x ( x e. A /\ ps ) <-> E. y A. x ( ( x e. A /\ ps ) -> x = y ) )
17 impexp 
 |-  ( ( ( x e. A /\ ps ) -> x = y ) <-> ( x e. A -> ( ps -> x = y ) ) )
18 17 albii 
 |-  ( A. x ( ( x e. A /\ ps ) -> x = y ) <-> A. x ( x e. A -> ( ps -> x = y ) ) )
19 df-ral 
 |-  ( A. x e. A ( ps -> x = y ) <-> A. x ( x e. A -> ( ps -> x = y ) ) )
20 18 19 bitr4i 
 |-  ( A. x ( ( x e. A /\ ps ) -> x = y ) <-> A. x e. A ( ps -> x = y ) )
21 20 exbii 
 |-  ( E. y A. x ( ( x e. A /\ ps ) -> x = y ) <-> E. y A. x e. A ( ps -> x = y ) )
22 15 16 21 3bitri 
 |-  ( E* x e. A ps <-> E. y A. x e. A ( ps -> x = y ) )
23 22 imbi2i 
 |-  ( ( ph -> E* x e. A ps ) <-> ( ph -> E. y A. x e. A ( ps -> x = y ) ) )
24 19.37v 
 |-  ( E. y ( ph -> A. x e. A ( ps -> x = y ) ) <-> ( ph -> E. y A. x e. A ( ps -> x = y ) ) )
25 23 24 bitr4i 
 |-  ( ( ph -> E* x e. A ps ) <-> E. y ( ph -> A. x e. A ( ps -> x = y ) ) )
26 6 14 25 3bitr4i 
 |-  ( E* x e. A ( ph /\ ps ) <-> ( ph -> E* x e. A ps ) )