Metamath Proof Explorer


Theorem axrep4

Description: A more traditional version of the Axiom of Replacement. (Contributed by NM, 14-Aug-1994) (Proof shortened by Matthew House, 18-Sep-2025)

Ref Expression
Hypothesis axrep4.1 z φ
Assertion axrep4 x z y φ y = z z y y z x x w φ

Proof

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