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

Step	Hyp	Ref	Expression
0		cgzr	|- AxRep
1		vu	|- u
2		cfmla	|- Fmla
3		com	|- _om
4	3 2	cfv	|- ( Fmla ` _om )
5		c3o	|- 3o
6		c1o	|- 1o
7		c2o	|- 2o
8	1	cv	|- u
9	8 6	cgol	|- A.g 1o u
10		cgoi	|- ->g
11		cgoq	|- =g
12	7 6 11	co	|- ( 2o =g 1o )
13	9 12 10	co	|- ( A.g 1o u ->g ( 2o =g 1o ) )
14	13 7	cgol	|- A.g 2o ( A.g 1o u ->g ( 2o =g 1o ) )
15	14 6	cgox	|- E.g 1o A.g 2o ( A.g 1o u ->g ( 2o =g 1o ) )
16	15 5	cgol	|- A.g 3o E.g 1o A.g 2o ( A.g 1o u ->g ( 2o =g 1o ) )
17		cgoe	|- e.g
18	7 6 17	co	|- ( 2o e.g 1o )
19		cgob	|- <->g
20		c0	|- (/)
21	5 20 17	co	|- ( 3o e.g (/) )
22		cgoa	|- /\g
23	21 9 22	co	|- ( ( 3o e.g (/) ) /\g A.g 1o u )
24	23 5	cgox	|- E.g 3o ( ( 3o e.g (/) ) /\g A.g 1o u )
25	18 24 19	co	|- ( ( 2o e.g 1o ) <->g E.g 3o ( ( 3o e.g (/) ) /\g A.g 1o u ) )
26	25 7	cgol	|- A.g 2o ( ( 2o e.g 1o ) <->g E.g 3o ( ( 3o e.g (/) ) /\g A.g 1o u ) )
27	26 6	cgol	|- A.g 1o A.g 2o ( ( 2o e.g 1o ) <->g E.g 3o ( ( 3o e.g (/) ) /\g A.g 1o u ) )
28	16 27 10	co	|- ( 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 ) ) )
29	1 4 28	cmpt	|- ( 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 ) ) ) )
30	0 29	wceq	|- 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 ) ) ) )