Definition df-gzf 33321

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 33314	. 2 class ZF
2		vm	. . . . . . 7 setvar 𝑚
3	2	cv 1538	. . . . . 6 class 𝑚
4	3	wtr 5187	. . . . 5 wff Tr 𝑚
5		cgze 33308	. . . . . 6 class AxExt
6		cprv 33201	. . . . . 6 class ⊧
7	3, 5, 6	wbr 5070	. . . . 5 wff 𝑚⊧AxExt
8		cgzp 33310	. . . . . 6 class AxPow
9	3, 8, 6	wbr 5070	. . . . 5 wff 𝑚⊧AxPow
10	4, 7, 9	w3a 1085	. . . 4 wff (Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow)
11		cgzu 33311	. . . . . 6 class AxUn
12	3, 11, 6	wbr 5070	. . . . 5 wff 𝑚⊧AxUn
13		cgzg 33312	. . . . . 6 class AxReg
14	3, 13, 6	wbr 5070	. . . . 5 wff 𝑚⊧AxReg
15		cgzi 33313	. . . . . 6 class AxInf
16	3, 15, 6	wbr 5070	. . . . 5 wff 𝑚⊧AxInf
17	12, 14, 16	w3a 1085	. . . 4 wff (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf)
18		vu	. . . . . . . 8 setvar 𝑢
19	18	cv 1538	. . . . . . 7 class 𝑢
20		cgzr 33309	. . . . . . 7 class AxRep
21	19, 20	cfv 6418	. . . . . 6 class (AxRep‘𝑢)
22	3, 21, 6	wbr 5070	. . . . 5 wff 𝑚⊧(AxRep‘𝑢)
23		com 7687	. . . . . 6 class ω
24		cfmla 33199	. . . . . 6 class Fmla
25	23, 24	cfv 6418	. . . . 5 class (Fmla‘ω)
26	22, 18, 25	wral 3063	. . . 4 wff ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢)
27	10, 17, 26	w3a 1085	. . 3 wff ((Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))
28	27, 2	cab 2715	. 2 class {𝑚 ∣ ((Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))}
29	1, 28	wceq 1539	1 wff ZF = {𝑚 ∣ ((Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))}

This definition is referenced by: (None)