  CZF and IZF are formulated on the basis of  intuitionistic first-order logic with equality, having only \(\in\) (membership) as an additional non-logical binary predicate symbol. Their set-theoretic axioms are as follows.