ax-ext

Axiom.

Arguments:

a (st), b (st), x (sv),

Distinct variable conditions:

(x, a), (x, b),

Assertions:

(forallx((xina)leftrightarrow(xinb))to(aeqb))