bound in 
)Top-level context. Extensionality
Theorems for collections (symbol kind 'coll') whose equality predicate satisfies the Axiom of Extensionality.
| Name | Sym | Comment |
| df-bvt | ( bound in ) |
| Name | Comment |
| bv-= | |
| ceqd | |
| ceqi | |
| eq-refl | |
| eq.sub | |
| eqt< | |
| eqt<> | |
| eqt<>d | |
| eqt<>i | |
| eqt<a | |
| eqt> | |
| equf | |
| neq< | |
| neq> | |
| ord-ax-refl | |
| rp-1< | |
| rp-1<d | |
| rp-1> | |
| rp-1>d | |
| rp-2< | |
| rp-2<d | |
| rp-2<g | |
| rp-2> | |
| rp-2>d | |
| sub-refl | |
| sub-tr |
| Name | Comment |
| ceq | |
| provide-order-ax | Axioms for partial order relations |
| sub |