Definition df-gzf 35464

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

Assertion

Ref	Expression
df-gzf	⊢ ZF = {𝑚 ∣ ((Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))}

Distinct variable group:   𝑢,𝑚

Detailed syntax breakdown of Definition df-gzf

Step	Hyp	Ref	Expression
1		cgzf 35457	. 2 class ZF
2		vm	. . . . . . 7 setvar 𝑚
3	2	cv 1539	. . . . . 6 class 𝑚
4	3	wtr 5259	. . . . 5 wff Tr 𝑚
5		cgze 35451	. . . . . 6 class AxExt
6		cprv 35344	. . . . . 6 class ⊧
7	3, 5, 6	wbr 5143	. . . . 5 wff 𝑚⊧AxExt
8		cgzp 35453	. . . . . 6 class AxPow
9	3, 8, 6	wbr 5143	. . . . 5 wff 𝑚⊧AxPow
10	4, 7, 9	w3a 1087	. . . 4 wff (Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow)
11		cgzu 35454	. . . . . 6 class AxUn
12	3, 11, 6	wbr 5143	. . . . 5 wff 𝑚⊧AxUn
13		cgzg 35455	. . . . . 6 class AxReg
14	3, 13, 6	wbr 5143	. . . . 5 wff 𝑚⊧AxReg
15		cgzi 35456	. . . . . 6 class AxInf
16	3, 15, 6	wbr 5143	. . . . 5 wff 𝑚⊧AxInf
17	12, 14, 16	w3a 1087	. . . 4 wff (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf)
18		vu	. . . . . . . 8 setvar 𝑢
19	18	cv 1539	. . . . . . 7 class 𝑢
20		cgzr 35452	. . . . . . 7 class AxRep
21	19, 20	cfv 6561	. . . . . 6 class (AxRep‘𝑢)
22	3, 21, 6	wbr 5143	. . . . 5 wff 𝑚⊧(AxRep‘𝑢)
23		com 7887	. . . . . 6 class ω
24		cfmla 35342	. . . . . 6 class Fmla
25	23, 24	cfv 6561	. . . . 5 class (Fmla‘ω)
26	22, 18, 25	wral 3061	. . . 4 wff ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢)
27	10, 17, 26	w3a 1087	. . 3 wff ((Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))
28	27, 2	cab 2714	. 2 class {𝑚 ∣ ((Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))}
29	1, 28	wceq 1540	1 wff ZF = {𝑚 ∣ ((Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))}

This definition is referenced by: (None)