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 )