Metamath Proof Explorer


Theorem axrep4v

Description: Version of axrep4 with a disjoint variable condition, requiring fewer axioms. (Contributed by Matthew House, 18-Sep-2025)

Ref Expression
Assertion axrep4v x z y φ y = z z y y z x x w φ

Proof

Step Hyp Ref Expression
1 ax-rep x z y z φ y = z z y y z x x w z φ
2 19.3v z φ φ
3 2 imbi1i z φ y = z φ y = z
4 3 albii y z φ y = z y φ y = z
5 4 exbii z y z φ y = z z y φ y = z
6 5 albii x z y z φ y = z x z y φ y = z
7 2 anbi2i x w z φ x w φ
8 7 exbii x x w z φ x x w φ
9 8 bibi2i y z x x w z φ y z x x w φ
10 9 albii y y z x x w z φ y y z x x w φ
11 10 exbii z y y z x x w z φ z y y z x x w φ
12 1 6 11 3imtr3i x z y φ y = z z y y z x x w φ