# Metamath Proof Explorer

## Definition df-gzf

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

Ref Expression
Assertion df-gzf ${⊢}\mathbf{ZF}=\left\{{m}|\left(\left(\mathrm{Tr}{m}\wedge {m}\vDash \mathrm{AxExt}\wedge {m}\vDash \mathrm{AxPow}\right)\wedge \left({m}\vDash \mathrm{AxUn}\wedge {m}\vDash \mathrm{AxReg}\wedge {m}\vDash \mathrm{AxInf}\right)\wedge \forall {u}\in \mathrm{Fmla}\left(\mathrm{\omega }\right)\phantom{\rule{.4em}{0ex}}{m}\vDash \mathrm{AxRep}\left({u}\right)\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cgzf ${class}\mathbf{ZF}$
1 vm ${setvar}{m}$
2 1 cv ${setvar}{m}$
3 2 wtr ${wff}\mathrm{Tr}{m}$
4 cprv ${class}\vDash$
5 cgze ${class}\mathrm{AxExt}$
6 2 5 4 wbr ${wff}{m}\vDash \mathrm{AxExt}$
7 cgzp ${class}\mathrm{AxPow}$
8 2 7 4 wbr ${wff}{m}\vDash \mathrm{AxPow}$
9 3 6 8 w3a ${wff}\left(\mathrm{Tr}{m}\wedge {m}\vDash \mathrm{AxExt}\wedge {m}\vDash \mathrm{AxPow}\right)$
10 cgzu ${class}\mathrm{AxUn}$
11 2 10 4 wbr ${wff}{m}\vDash \mathrm{AxUn}$
12 cgzg ${class}\mathrm{AxReg}$
13 2 12 4 wbr ${wff}{m}\vDash \mathrm{AxReg}$
14 cgzi ${class}\mathrm{AxInf}$
15 2 14 4 wbr ${wff}{m}\vDash \mathrm{AxInf}$
16 11 13 15 w3a ${wff}\left({m}\vDash \mathrm{AxUn}\wedge {m}\vDash \mathrm{AxReg}\wedge {m}\vDash \mathrm{AxInf}\right)$
17 vu ${setvar}{u}$
18 cfmla ${class}\mathrm{Fmla}$
19 com ${class}\mathrm{\omega }$
20 19 18 cfv ${class}\mathrm{Fmla}\left(\mathrm{\omega }\right)$
21 cgzr ${class}\mathrm{AxRep}$
22 17 cv ${setvar}{u}$
23 22 21 cfv ${class}\mathrm{AxRep}\left({u}\right)$
24 2 23 4 wbr ${wff}{m}\vDash \mathrm{AxRep}\left({u}\right)$
25 24 17 20 wral ${wff}\forall {u}\in \mathrm{Fmla}\left(\mathrm{\omega }\right)\phantom{\rule{.4em}{0ex}}{m}\vDash \mathrm{AxRep}\left({u}\right)$
26 9 16 25 w3a ${wff}\left(\left(\mathrm{Tr}{m}\wedge {m}\vDash \mathrm{AxExt}\wedge {m}\vDash \mathrm{AxPow}\right)\wedge \left({m}\vDash \mathrm{AxUn}\wedge {m}\vDash \mathrm{AxReg}\wedge {m}\vDash \mathrm{AxInf}\right)\wedge \forall {u}\in \mathrm{Fmla}\left(\mathrm{\omega }\right)\phantom{\rule{.4em}{0ex}}{m}\vDash \mathrm{AxRep}\left({u}\right)\right)$
27 26 1 cab ${class}\left\{{m}|\left(\left(\mathrm{Tr}{m}\wedge {m}\vDash \mathrm{AxExt}\wedge {m}\vDash \mathrm{AxPow}\right)\wedge \left({m}\vDash \mathrm{AxUn}\wedge {m}\vDash \mathrm{AxReg}\wedge {m}\vDash \mathrm{AxInf}\right)\wedge \forall {u}\in \mathrm{Fmla}\left(\mathrm{\omega }\right)\phantom{\rule{.4em}{0ex}}{m}\vDash \mathrm{AxRep}\left({u}\right)\right)\right\}$
28 0 27 wceq ${wff}\mathbf{ZF}=\left\{{m}|\left(\left(\mathrm{Tr}{m}\wedge {m}\vDash \mathrm{AxExt}\wedge {m}\vDash \mathrm{AxPow}\right)\wedge \left({m}\vDash \mathrm{AxUn}\wedge {m}\vDash \mathrm{AxReg}\wedge {m}\vDash \mathrm{AxInf}\right)\wedge \forall {u}\in \mathrm{Fmla}\left(\mathrm{\omega }\right)\phantom{\rule{.4em}{0ex}}{m}\vDash \mathrm{AxRep}\left({u}\right)\right)\right\}$