Metamath Proof Explorer

Theorem lncnbd

Description: A continuous linear operator is a bounded linear operator. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion lncnbd 
|- ( LinOp i^i ContOp ) = BndLinOp

Proof

Step Hyp Ref Expression
1 lncnopbd 
 |-  ( t e. ( LinOp i^i ContOp ) <-> t e. BndLinOp )
2 1 eqriv 
 |-  ( LinOp i^i ContOp ) = BndLinOp