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

Metamath Proof Explorer

Theorem rmoanimALT

Description: Alternate proof of rmoanim , shorter but requiring ax-10 and ax-11 . (Contributed by Alexander van der Vekens, 25-Jun-2017) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis rmoanim.1 
|- F/ x ph
Assertion rmoanimALT 
|- ( 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 nfv 
 |-  F/ y ( ph /\ ps )
8 7 rmo2 
 |-  ( E* x e. A ( ph /\ ps ) <-> E. y A. x e. A ( ( ph /\ ps ) -> x = y ) )
9 nfv 
 |-  F/ y ps
10 9 rmo2 
 |-  ( E* x e. A ps <-> E. y A. x e. A ( ps -> x = y ) )
11 10 imbi2i 
 |-  ( ( ph -> E* x e. A ps ) <-> ( ph -> E. y A. x e. A ( ps -> x = y ) ) )
12 19.37v 
 |-  ( E. y ( ph -> A. x e. A ( ps -> x = y ) ) <-> ( ph -> E. y A. x e. A ( ps -> x = y ) ) )
13 11 12 bitr4i 
 |-  ( ( ph -> E* x e. A ps ) <-> E. y ( ph -> A. x e. A ( ps -> x = y ) ) )
14 6 8 13 3bitr4i 
 |-  ( E* x e. A ( ph /\ ps ) <-> ( ph -> E* x e. A ps ) )