Metamath Proof Explorer


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 ) ) ) ) )