Definition df-gzrep 31351

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.)

Assertion

Ref	Expression
df-gzrep	|- AxRep = ( u e. ( Fmla ` om ) |-> ( A.g 3o E.g 1o A.g 2o ( A.g 1o u ->g ( 2o =g 1o ) ) ->g A.g 1o A.g 2o ( ( 2o e.g 1o ) <->g E.g 3o ( ( 3o e.g (/) ) /\g A.g 1o u ) ) ) )

Detailed syntax breakdown of Definition df-gzrep

Step	Hyp	Ref	Expression
1		cgzr 31344	. 2 class AxRep
2		vu	. . 3 setvar u
3		com 7065	. . . 4 class om
4		cfmla 31319	. . . 4 class Fmla
5	3, 4	cfv 5888	. . 3 class ( Fmla ` om )
6	2	cv 1482	. . . . . . . . 9 class u
7		c1o 7553	. . . . . . . . 9 class 1o
8	6, 7	cgol 31317	. . . . . . . 8 class A.g 1o u
9		c2o 7554	. . . . . . . . 9 class 2o
10		cgoq 31333	. . . . . . . . 9 class =g
11	9, 7, 10	co 6650	. . . . . . . 8 class ( 2o =g 1o )
12		cgoi 31330	. . . . . . . 8 class ->g
13	8, 11, 12	co 6650	. . . . . . 7 class ( A.g 1o u ->g ( 2o =g 1o ) )
14	13, 9	cgol 31317	. . . . . 6 class A.g 2o ( A.g 1o u ->g ( 2o =g 1o ) )
15	14, 7	cgox 31334	. . . . 5 class E.g 1o A.g 2o ( A.g 1o u ->g ( 2o =g 1o ) )
16		c3o 7555	. . . . 5 class 3o
17	15, 16	cgol 31317	. . . 4 class A.g 3o E.g 1o A.g 2o ( A.g 1o u ->g ( 2o =g 1o ) )
18		cgoe 31315	. . . . . . . 8 class e.g
19	9, 7, 18	co 6650	. . . . . . 7 class ( 2o e.g 1o )
20		c0 3915	. . . . . . . . . 10 class (/)
21	16, 20, 18	co 6650	. . . . . . . . 9 class ( 3o e.g (/) )
22		cgoa 31329	. . . . . . . . 9 class /\g
23	21, 8, 22	co 6650	. . . . . . . 8 class ( ( 3o e.g (/) ) /\g A.g 1o u )
24	23, 16	cgox 31334	. . . . . . 7 class E.g 3o ( ( 3o e.g (/) ) /\g A.g 1o u )
25		cgob 31332	. . . . . . 7 class <->g
26	19, 24, 25	co 6650	. . . . . 6 class ( ( 2o e.g 1o ) <->g E.g 3o ( ( 3o e.g (/) ) /\g A.g 1o u ) )
27	26, 9	cgol 31317	. . . . 5 class A.g 2o ( ( 2o e.g 1o ) <->g E.g 3o ( ( 3o e.g (/) ) /\g A.g 1o u ) )
28	27, 7	cgol 31317	. . . 4 class A.g 1o A.g 2o ( ( 2o e.g 1o ) <->g E.g 3o ( ( 3o e.g (/) ) /\g A.g 1o u ) )
29	17, 28, 12	co 6650	. . 3 class ( A.g 3o E.g 1o A.g 2o ( A.g 1o u ->g ( 2o =g 1o ) ) ->g A.g 1o A.g 2o ( ( 2o e.g 1o ) <->g E.g 3o ( ( 3o e.g (/) ) /\g A.g 1o u ) ) )
30	2, 5, 29	cmpt 4729	. 2 class ( u e. ( Fmla ` om ) |-> ( A.g 3o E.g 1o A.g 2o ( A.g 1o u ->g ( 2o =g 1o ) ) ->g A.g 1o A.g 2o ( ( 2o e.g 1o ) <->g E.g 3o ( ( 3o e.g (/) ) /\g A.g 1o u ) ) ) )
31	1, 30	wceq 1483	1 wff AxRep = ( u e. ( Fmla ` om ) |-> ( A.g 3o E.g 1o A.g 2o ( A.g 1o u ->g ( 2o =g 1o ) ) ->g A.g 1o A.g 2o ( ( 2o e.g 1o ) <->g E.g 3o ( ( 3o e.g (/) ) /\g A.g 1o u ) ) ) )

This definition is referenced by: (None)