Theorem axreplem

Description: Lemma for axrep2 and axrep3 . (Contributed by BJ, 6-Aug-2022)

	Ref	Expression
Assertion	axreplem	|- ( x = y -> ( E. u ( ph -> A. v ( ps <-> E. w ( z e. x /\ ch ) ) ) <-> E. u ( ph -> A. v ( ps <-> E. w ( z e. y /\ ch ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elequ2	|- ( x = y -> ( z e. x <-> z e. y ) )
2	1	anbi1d	|- ( x = y -> ( ( z e. x /\ ch ) <-> ( z e. y /\ ch ) ) )
3	2	exbidv	|- ( x = y -> ( E. w ( z e. x /\ ch ) <-> E. w ( z e. y /\ ch ) ) )
4	3	bibi2d	|- ( x = y -> ( ( ps <-> E. w ( z e. x /\ ch ) ) <-> ( ps <-> E. w ( z e. y /\ ch ) ) ) )
5	4	albidv	|- ( x = y -> ( A. v ( ps <-> E. w ( z e. x /\ ch ) ) <-> A. v ( ps <-> E. w ( z e. y /\ ch ) ) ) )
6	5	imbi2d	|- ( x = y -> ( ( ph -> A. v ( ps <-> E. w ( z e. x /\ ch ) ) ) <-> ( ph -> A. v ( ps <-> E. w ( z e. y /\ ch ) ) ) ) )
7	6	exbidv	|- ( x = y -> ( E. u ( ph -> A. v ( ps <-> E. w ( z e. x /\ ch ) ) ) <-> E. u ( ph -> A. v ( ps <-> E. w ( z e. y /\ ch ) ) ) ) )