Metamath Proof Explorer

Theorem bracl

Description: Closure of the bra function. (Contributed by NM, 23-May-2006) (New usage is discouraged.)

Ref Expression
Assertion bracl 
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( bra ` A ) ` B ) e. CC )

Proof

Step Hyp Ref Expression
1 brafn 
 |-  ( A e. ~H -> ( bra ` A ) : ~H --> CC )
2 1 ffvelcdmda 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( bra ` A ) ` B ) e. CC )