Нехай А - множина, і P(x,y) - предикат. Тоді якщо для кожного x існує єдиний y, такий що P(x,y) істинний, тоді існує множина всіх y, для яких знайдеться такий x ∈ A, що P(x,y) істинний.
Зв'язок з іншими аксіомами
Аксіома не потрібна для більшості доведень, її зазвичай не включають в системи теорії типів.