Metamath Proof Explorer

Theorem clintop

Description: A closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020)

Ref Expression
Assertion clintop 
|- ( .o. e. ( clIntOp ` M ) -> .o. : ( M X. M ) --> M )

Proof

Step Hyp Ref Expression
1 elfvex 
 |-  ( .o. e. ( clIntOp ` M ) -> M e. _V )
2 isclintop 
 |-  ( M e. _V -> ( .o. e. ( clIntOp ` M ) <-> .o. : ( M X. M ) --> M ) )
3 2 biimpd 
 |-  ( M e. _V -> ( .o. e. ( clIntOp ` M ) -> .o. : ( M X. M ) --> M ) )
4 1 3 mpcom 
 |-  ( .o. e. ( clIntOp ` M ) -> .o. : ( M X. M ) --> M )