Editing Zermelo–Fraenkel set theory (section)

===Virtual classes===

Proper classes (collections of mathematical objects defined by a property shared by their members which are too big to be sets) can only be treated indirectly in ZF (and thus ZFC).
An alternative to proper classes while staying within ZF and ZFC is the ''virtual class'' notational construct introduced by {{harvtxt|Quine|1969}}, where the entire construct ''y'' &isin; { ''x'' | F''x'' } is simply defined as F''y''.<ref>{{harvnb|Link|2014}}</ref> This provides a simple notation for classes that can contain sets but need not themselves be sets, while not committing to the ontology of classes (because the notation can be syntactically converted to one that only uses sets).  Quine's approach built on the earlier approach of {{harvtxt|Bernays|Fraenkel|1958}}.  Virtual classes are also used in {{harvtxt|Levy|2002}}, {{harvtxt|Takeuti|Zaring|1982}}, and in the [[Metamath]] implementation of ZFC.