Nechť x nemá v A volný výskyt
A ↔ (∀x)A
Budu dokazovat dvě implikace
|- A→(∀x)A a |- (∀x)A→A
→
Vyjdu z v1
|- A→A
Podle věty o zavedení obecného kvantifikátoru
|- A→(∀x)A
←
Vyjdu ze schematu specifikace
|- (∀x)A→Ax[t]
Za t dosadím x
|- (∀x)A→A
QED
Nechť x nemá v A volný výskyt
(∃x)A↔A
Stejně jako v předchozím případě budu dokazovat dvě implikace
(∃x)A→A a A→(∃x)A
→
Vyjdu z
|- A→A
Podle věty o zavedení existenčního kvantifikátoru
|- (∃x)A→A
←
Podle pravidla substituce
|- Ax[t]→(∃x)A
Za t dosadím x
|- A→(∃x)A
QED