Metamath Proof Explorer


Theorem axrep6

Description: A condensed form of ax-rep . (Contributed by SN, 18-Sep-2023) (Proof shortened by Matthew House, 18-Sep-2025)

Ref Expression
Assertion axrep6 w * z φ y z z y w x φ

Proof

Step Hyp Ref Expression
1 axrep4v w y z φ z = y y z z y w w x φ
2 df-mo * z φ y z φ z = y
3 2 albii w * z φ w y z φ z = y
4 df-rex w x φ w w x φ
5 4 bibi2i z y w x φ z y w w x φ
6 5 albii z z y w x φ z z y w w x φ
7 6 exbii y z z y w x φ y z z y w w x φ
8 1 3 7 3imtr4i w * z φ y z z y w x φ