sbex

Theorem.

Arguments:

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

Distinct variable conditions:

(z, a), (z, x),

Assertions:

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

Proof:

Hyp Ref Line Expr
sb-neg1([a/x]lnotforallzlnotphileftrightarrowlnot[a/x]forallzlnotphi)
sbal2([a/x]forallzlnotphileftrightarrowforallz[a/x]lnotphi)
sb-neg3([a/x]lnotphileftrightarrowlnot[a/x]phi)
3eqt-∀-i4(forallz[a/x]lnotphileftrightarrowforallzlnot[a/x]phi)
2, 4bitr5([a/x]forallzlnotphileftrightarrowforallzlnot[a/x]phi)
5bi.bldneg6(lnot[a/x]forallzlnotphileftrightarrowlnotforallzlnot[a/x]phi)
1, 6bitr7([a/x]lnotforallzlnotphileftrightarrowlnotforallzlnot[a/x]phi)
df-ex8(existszphileftrightarrowlnotforallzlnotphi)
8bi.bldsb9([a/x]existszphileftrightarrow[a/x]lnotforallzlnotphi)
df-ex10(existsz[a/x]phileftrightarrowlnotforallzlnot[a/x]phi)
7, 9, 10<2bitr11([a/x]existszphileftrightarrowexistsz[a/x]phi)