sbal

Theorem.

Arguments:

a (st), x (sv), z (sv), phi (pr),

Dummy variables:

w (sv),

Distinct variable conditions:

(w, a), (w, x), (w, z), (w, phi), (z, a), (z, x),

Assertions:

([a/x]forallzphileftrightarrowforallz[a/x]phi)

Proof:

Hyp Ref Line Expr
sbal-w1([w/x]forallzphileftrightarrowforallz[w/x]phi)
1bi.bldsb2([a/w][w/x]forallzphileftrightarrow[a/w]forallz[w/x]phi)
sbal-w3([a/w]forallz[w/x]phileftrightarrowforallz[a/w][w/x]phi)
2, 3bitr4([a/w][w/x]forallzphileftrightarrowforallz[a/w][w/x]phi)
sbco2w5([a/w][w/x]phileftrightarrow[a/x]phi)
5eqt-∀-i6(forallz[a/w][w/x]phileftrightarrowforallz[a/x]phi)
sbco2w7([a/w][w/x]forallzphileftrightarrow[a/x]forallzphi)
4, 6, 7>2bitr8([a/x]forallzphileftrightarrowforallz[a/x]phi)