Metamath Proof Explorer


Theorem axrep3

Description: Axiom of Replacement slightly strengthened from axrep2 ; w may occur free in ph . (Contributed by NM, 2-Jan-1997) Remove dependency on ax-13 . (Revised by BJ, 31-May-2019)

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

Proof

Step Hyp Ref Expression
1 nfe1 y y z φ z = y
2 nfv y z x
3 nfv y x w
4 nfa1 y y φ
5 3 4 nfan y x w y φ
6 5 nfex y x x w y φ
7 2 6 nfbi y z x x x w y φ
8 7 nfal y z z x x x w y φ
9 1 8 nfim y y z φ z = y z z x x x w y φ
10 9 nfex y x y z φ z = y z z x x x w y φ
11 axreplem y = w x y z φ z = y z z x x x y y φ x y z φ z = y z z x x x w y φ
12 axrep2 x y z φ z = y z z x x x y y φ
13 10 11 12 chvarfv x y z φ z = y z z x x x w y φ