Metamath Proof Explorer


Definition df-gzrep

Description: The Godel-set version of the Axiom Scheme of Replacement. Since this is a scheme and not a single axiom, it manifests as a function on wffs, each giving rise to a different axiom. (Contributed by Mario Carneiro, 14-Jul-2013)

Ref Expression
Assertion df-gzrep AxRep = u Fmla ω 𝑔 3 𝑜 𝑔 1 𝑜 𝑔 2 𝑜 𝑔 1 𝑜 u 𝑔 2 𝑜 = 𝑔 1 𝑜 𝑔 𝑔 1 𝑜 𝑔 2 𝑜 2 𝑜 𝑔 1 𝑜 𝑔 𝑔 3 𝑜 3 𝑜 𝑔 𝑔 𝑔 1 𝑜 u

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgzr class AxRep
1 vu setvar u
2 cfmla class Fmla
3 com class ω
4 3 2 cfv class Fmla ω
5 c3o class 3 𝑜
6 c1o class 1 𝑜
7 c2o class 2 𝑜
8 1 cv setvar u
9 8 6 cgol class 𝑔 1 𝑜 u
10 cgoi class 𝑔
11 cgoq class = 𝑔
12 7 6 11 co class 2 𝑜 = 𝑔 1 𝑜
13 9 12 10 co class 𝑔 1 𝑜 u 𝑔 2 𝑜 = 𝑔 1 𝑜
14 13 7 cgol class 𝑔 2 𝑜 𝑔 1 𝑜 u 𝑔 2 𝑜 = 𝑔 1 𝑜
15 14 6 cgox class 𝑔 1 𝑜 𝑔 2 𝑜 𝑔 1 𝑜 u 𝑔 2 𝑜 = 𝑔 1 𝑜
16 15 5 cgol class 𝑔 3 𝑜 𝑔 1 𝑜 𝑔 2 𝑜 𝑔 1 𝑜 u 𝑔 2 𝑜 = 𝑔 1 𝑜
17 cgoe class 𝑔
18 7 6 17 co class 2 𝑜 𝑔 1 𝑜
19 cgob class 𝑔
20 c0 class
21 5 20 17 co class 3 𝑜 𝑔
22 cgoa class 𝑔
23 21 9 22 co class 3 𝑜 𝑔 𝑔 𝑔 1 𝑜 u
24 23 5 cgox class 𝑔 3 𝑜 3 𝑜 𝑔 𝑔 𝑔 1 𝑜 u
25 18 24 19 co class 2 𝑜 𝑔 1 𝑜 𝑔 𝑔 3 𝑜 3 𝑜 𝑔 𝑔 𝑔 1 𝑜 u
26 25 7 cgol class 𝑔 2 𝑜 2 𝑜 𝑔 1 𝑜 𝑔 𝑔 3 𝑜 3 𝑜 𝑔 𝑔 𝑔 1 𝑜 u
27 26 6 cgol class 𝑔 1 𝑜 𝑔 2 𝑜 2 𝑜 𝑔 1 𝑜 𝑔 𝑔 3 𝑜 3 𝑜 𝑔 𝑔 𝑔 1 𝑜 u
28 16 27 10 co class 𝑔 3 𝑜 𝑔 1 𝑜 𝑔 2 𝑜 𝑔 1 𝑜 u 𝑔 2 𝑜 = 𝑔 1 𝑜 𝑔 𝑔 1 𝑜 𝑔 2 𝑜 2 𝑜 𝑔 1 𝑜 𝑔 𝑔 3 𝑜 3 𝑜 𝑔 𝑔 𝑔 1 𝑜 u
29 1 4 28 cmpt class u Fmla ω 𝑔 3 𝑜 𝑔 1 𝑜 𝑔 2 𝑜 𝑔 1 𝑜 u 𝑔 2 𝑜 = 𝑔 1 𝑜 𝑔 𝑔 1 𝑜 𝑔 2 𝑜 2 𝑜 𝑔 1 𝑜 𝑔 𝑔 3 𝑜 3 𝑜 𝑔 𝑔 𝑔 1 𝑜 u
30 0 29 wceq wff AxRep = u Fmla ω 𝑔 3 𝑜 𝑔 1 𝑜 𝑔 2 𝑜 𝑔 1 𝑜 u 𝑔 2 𝑜 = 𝑔 1 𝑜 𝑔 𝑔 1 𝑜 𝑔 2 𝑜 2 𝑜 𝑔 1 𝑜 𝑔 𝑔 3 𝑜 3 𝑜 𝑔 𝑔 𝑔 1 𝑜 u