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

Metamath Proof Explorer

Theorem rexraleqim

Description: Statement following from existence and generalization with equality. (Contributed by AV, 9-Feb-2019)

Ref Expression
Hypotheses rexraleqim.1 
|- ( x = z -> ( ps <-> ph ) )
rexraleqim.2 
|- ( z = Y -> ( ph <-> th ) )
Assertion rexraleqim 
|- ( ( E. z e. A ph /\ A. x e. A ( ps -> x = Y ) ) -> th )

Proof

Step Hyp Ref Expression
1 rexraleqim.1 
 |-  ( x = z -> ( ps <-> ph ) )
2 rexraleqim.2 
 |-  ( z = Y -> ( ph <-> th ) )
3 eqeq1 
 |-  ( x = z -> ( x = Y <-> z = Y ) )
4 1 3 imbi12d 
 |-  ( x = z -> ( ( ps -> x = Y ) <-> ( ph -> z = Y ) ) )
5 4 rspcva 
 |-  ( ( z e. A /\ A. x e. A ( ps -> x = Y ) ) -> ( ph -> z = Y ) )
6 2 biimpd 
 |-  ( z = Y -> ( ph -> th ) )
7 5 6 syli 
 |-  ( ( z e. A /\ A. x e. A ( ps -> x = Y ) ) -> ( ph -> th ) )
8 7 impancom 
 |-  ( ( z e. A /\ ph ) -> ( A. x e. A ( ps -> x = Y ) -> th ) )
9 8 rexlimiva 
 |-  ( E. z e. A ph -> ( A. x e. A ( ps -> x = Y ) -> th ) )
10 9 imp 
 |-  ( ( E. z e. A ph /\ A. x e. A ( ps -> x = Y ) ) -> th )