Definition df-gzreg 31354

Description: The Godel-set version of the Axiom of Regularity. (Contributed by Mario Carneiro, 14-Jul-2013.)

Assertion

Ref	Expression
df-gzreg	|- AxReg = ( E.g 1o ( 1o e.g (/) ) ->g E.g 1o ( ( 1o e.g (/) ) /\g A.g 2o ( ( 2o e.g 1o ) ->g -.g ( 2o e.g (/) ) ) ) )

Detailed syntax breakdown of Definition df-gzreg

Step	Hyp	Ref	Expression
1		cgzg 31347	. 2 class AxReg
2		c1o 7553	. . . . 5 class 1o
3		c0 3915	. . . . 5 class (/)
4		cgoe 31315	. . . . 5 class e.g
5	2, 3, 4	co 6650	. . . 4 class ( 1o e.g (/) )
6	5, 2	cgox 31334	. . 3 class E.g 1o ( 1o e.g (/) )
7		c2o 7554	. . . . . . . 8 class 2o
8	7, 2, 4	co 6650	. . . . . . 7 class ( 2o e.g 1o )
9	7, 3, 4	co 6650	. . . . . . . 8 class ( 2o e.g (/) )
10	9	cgon 31328	. . . . . . 7 class -.g ( 2o e.g (/) )
11		cgoi 31330	. . . . . . 7 class ->g
12	8, 10, 11	co 6650	. . . . . 6 class ( ( 2o e.g 1o ) ->g -.g ( 2o e.g (/) ) )
13	12, 7	cgol 31317	. . . . 5 class A.g 2o ( ( 2o e.g 1o ) ->g -.g ( 2o e.g (/) ) )
14		cgoa 31329	. . . . 5 class /\g
15	5, 13, 14	co 6650	. . . 4 class ( ( 1o e.g (/) ) /\g A.g 2o ( ( 2o e.g 1o ) ->g -.g ( 2o e.g (/) ) ) )
16	15, 2	cgox 31334	. . 3 class E.g 1o ( ( 1o e.g (/) ) /\g A.g 2o ( ( 2o e.g 1o ) ->g -.g ( 2o e.g (/) ) ) )
17	6, 16, 11	co 6650	. 2 class ( E.g 1o ( 1o e.g (/) ) ->g E.g 1o ( ( 1o e.g (/) ) /\g A.g 2o ( ( 2o e.g 1o ) ->g -.g ( 2o e.g (/) ) ) ) )
18	1, 17	wceq 1483	1 wff AxReg = ( E.g 1o ( 1o e.g (/) ) ->g E.g 1o ( ( 1o e.g (/) ) /\g A.g 2o ( ( 2o e.g 1o ) ->g -.g ( 2o e.g (/) ) ) ) )

This definition is referenced by: (None)