Reformulation of MK

Language: mono-sorted first order logic with equality ‘‘="  and membership ‘‘∈" , with the following axioms added:

Classes: ∀W⃗ ∃!X:X={y|ϕ∧∃Z(y∈Z)}

In English: every formula ϕ defines a unique class of all 

elements satisfying it.

Let ‘‘V"   represent the class of all elements.

Let ‘‘ON" be the class of all ordinals in V 

Define: R is ranking⟺ 

R:V→ON∧∀x∈V: R(x)=min {α|∀y∈x:α>R(y)}

Sets: X∈V⟺

      ∃ ranking R:{R(y)|y∈X}≉V

≈  denotes equinumerousity, i.e. existence of a bijection.

In English: an element is a class for which the class of all ranks of its elements is strictly subnumerous to the universe.

Infinity: ∃x∈V:x≠∅∧∀a∈x∃b∈x:b⊋a

There exists a nonempty element that 

is closed under existence of proper 

superset.