df-gzf - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-gzf		Structured version Visualization version Unicode version

Definition df-gzf 31356

Description: Define the class of all (transitive) models of ZF. (Contributed by Mario Carneiro, 14-Jul-2013.)

**Assertion**
Ref	Expression
df-gzf	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$

**Detailed syntax breakdown of Definition df-gzf**
Step	Hyp	Ref	Expression
1		cgzf 31349	. 2
2		vm	. . . . . . 7
3	2	cv 1482	. . . . . 6
4	3	wtr 4752	. . . . 5
5		cgze 31343	. . . . . 6
6		cprv 31321	. . . . . 6
7	3, 5, 6	wbr 4653	. . . . 5
8		cgzp 31345	. . . . . 6
9	3, 8, 6	wbr 4653	. . . . 5
10	4, 7, 9	w3a 1037	. . . 4 $/\$ $/\$
11		cgzu 31346	. . . . . 6
12	3, 11, 6	wbr 4653	. . . . 5
13		cgzg 31347	. . . . . 6
14	3, 13, 6	wbr 4653	. . . . 5
15		cgzi 31348	. . . . . 6
16	3, 15, 6	wbr 4653	. . . . 5
17	12, 14, 16	w3a 1037	. . . 4 $/\$ $/\$
18		vu	. . . . . . . 8
19	18	cv 1482	. . . . . . 7
20		cgzr 31344	. . . . . . 7
21	19, 20	cfv 5888	. . . . . 6
22	3, 21, 6	wbr 4653	. . . . 5
23		com 7065	. . . . . 6
24		cfmla 31319	. . . . . 6
25	23, 24	cfv 5888	. . . . 5
26	22, 18, 25	wral 2912	. . . 4
27	10, 17, 26	w3a 1037	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28	27, 2	cab 2608	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	1, 28	wceq 1483	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

This definition is referenced by: (None)