|- (∃y)(∀x)A→(∀x)(∃y)A
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