Vyjdu z

|- (∀y)¬A→¬A (důkaz někde na této wiki)

To lze napsat jako

|- ¬(∃y)A→¬A

Podle A3 a modus ponens

   ¬(∃y)A->¬A     (¬(∃y)A->¬A)->(A->(∃y)A)
  -----------------------------------------
                 A->(∃y)A

pozn.: (tohle je pravidlo substituce. - Kdyz bychom uz predpokladali, ze ho mame dokazane, muzeme vyjit rovnou z tohoto) (resp. to predtim je dukaz pravidla substituce)

|- A→(∃y)A

Podle předchozího lemmata o distribuci kvantifikátorů

|- (∀x)A→(∀x)(∃y)A

Dále y určitě nemá v (∀x)(∃y)A volný výskyt, tedy podle pravidla zavedení ∃

|- (∃y)(∀x)A→(∀x)(∃y)A

QED