eqt<>i

Theorem.

Arguments:

x (st), y (st), a (coll), b (coll),

Hypotheses:

(aequivb)
(xeqy)

Assertions:

((xina)leftrightarrow(yinb))

Proof:

Hyp Ref Line Expr
Hypo1(aequivb)
2(xeqy)
1, 2>andi3((xeqy)wedge(aequivb))
3eqt<>4((xina)leftrightarrow(yinb))