Metamath Proof Explorer


Theorem bj-ax12

Description: Remove a DV condition from bj-ax12v (using core axioms only). (Contributed by BJ, 26-Dec-2020) (Proof modification is discouraged.)

Ref Expression
Assertion bj-ax12 xx=tφxx=tφ

Proof

Step Hyp Ref Expression
1 bj-ax12v xx=yφxx=yφ
2 equequ2 y=tx=yx=t
3 2 imbi1d y=tx=yφx=tφ
4 3 albidv y=txx=yφxx=tφ
5 4 imbi2d y=tφxx=yφφxx=tφ
6 2 5 imbi12d y=tx=yφxx=yφx=tφxx=tφ
7 6 albidv y=txx=yφxx=yφxx=tφxx=tφ
8 1 7 mpbii y=txx=tφxx=tφ
9 ax6ev yy=t
10 8 9 exlimiiv xx=tφxx=tφ