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→A_x[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

|- A_x[t]→(∃x)A

Za t dosadím x

|- A→(∃x)A

QED