Definition df-gzf 33560

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 33553	. 2 class ZF
2		vm	. . . . . . 7 setvar 𝑚
3	2	cv 1539	. . . . . 6 class 𝑚
4	3	wtr 5204	. . . . 5 wff Tr 𝑚
5		cgze 33547	. . . . . 6 class AxExt
6		cprv 33440	. . . . . 6 class ⊧
7	3, 5, 6	wbr 5087	. . . . 5 wff 𝑚⊧AxExt
8		cgzp 33549	. . . . . 6 class AxPow
9	3, 8, 6	wbr 5087	. . . . 5 wff 𝑚⊧AxPow
10	4, 7, 9	w3a 1086	. . . 4 wff (Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow)
11		cgzu 33550	. . . . . 6 class AxUn
12	3, 11, 6	wbr 5087	. . . . 5 wff 𝑚⊧AxUn
13		cgzg 33551	. . . . . 6 class AxReg
14	3, 13, 6	wbr 5087	. . . . 5 wff 𝑚⊧AxReg
15		cgzi 33552	. . . . . 6 class AxInf
16	3, 15, 6	wbr 5087	. . . . 5 wff 𝑚⊧AxInf
17	12, 14, 16	w3a 1086	. . . 4 wff (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf)
18		vu	. . . . . . . 8 setvar 𝑢
19	18	cv 1539	. . . . . . 7 class 𝑢
20		cgzr 33548	. . . . . . 7 class AxRep
21	19, 20	cfv 6466	. . . . . 6 class (AxRep‘𝑢)
22	3, 21, 6	wbr 5087	. . . . 5 wff 𝑚⊧(AxRep‘𝑢)
23		com 7759	. . . . . 6 class ω
24		cfmla 33438	. . . . . 6 class Fmla
25	23, 24	cfv 6466	. . . . 5 class (Fmla‘ω)
26	22, 18, 25	wral 3062	. . . 4 wff ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢)
27	10, 17, 26	w3a 1086	. . 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)