Definition df-gzf 30610

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 30603	. 2 class ZF
2		vm	. . . . . . 7 setvar 𝑚
3	2	cv 1474	. . . . . 6 class 𝑚
4	3	wtr 4680	. . . . 5 wff Tr 𝑚
5		cgze 30597	. . . . . 6 class AxExt
6		cprv 30575	. . . . . 6 class ⊧
7	3, 5, 6	wbr 4583	. . . . 5 wff 𝑚⊧AxExt
8		cgzp 30599	. . . . . 6 class AxPow
9	3, 8, 6	wbr 4583	. . . . 5 wff 𝑚⊧AxPow
10	4, 7, 9	w3a 1031	. . . 4 wff (Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow)
11		cgzu 30600	. . . . . 6 class AxUn
12	3, 11, 6	wbr 4583	. . . . 5 wff 𝑚⊧AxUn
13		cgzg 30601	. . . . . 6 class AxReg
14	3, 13, 6	wbr 4583	. . . . 5 wff 𝑚⊧AxReg
15		cgzi 30602	. . . . . 6 class AxInf
16	3, 15, 6	wbr 4583	. . . . 5 wff 𝑚⊧AxInf
17	12, 14, 16	w3a 1031	. . . 4 wff (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf)
18		vu	. . . . . . . 8 setvar 𝑢
19	18	cv 1474	. . . . . . 7 class 𝑢
20		cgzr 30598	. . . . . . 7 class AxRep
21	19, 20	cfv 5804	. . . . . 6 class (AxRep‘𝑢)
22	3, 21, 6	wbr 4583	. . . . 5 wff 𝑚⊧(AxRep‘𝑢)
23		com 6957	. . . . . 6 class ω
24		cfmla 30573	. . . . . 6 class Fmla
25	23, 24	cfv 5804	. . . . 5 class (Fmla‘ω)
26	22, 18, 25	wral 2896	. . . 4 wff ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢)
27	10, 17, 26	w3a 1031	. . 3 wff ((Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))
28	27, 2	cab 2596	. 2 class {𝑚 ∣ ((Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))}
29	1, 28	wceq 1475	1 wff ZF = {𝑚 ∣ ((Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))}

This definition is referenced by: (None)