Theorem brafn

Description: The bra function is a functional. (Contributed by NM, 23-May-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	brafn	|- ( A e. ~H -> ( bra ` A ) : ~H --> CC )

Proof

Step	Hyp	Ref	Expression
1		brafval	|- ( A e. ~H -> ( bra ` A ) = ( x e. ~H |-> ( x .ih A ) ) )
2		hicl	|- ( ( x e. ~H /\ A e. ~H ) -> ( x .ih A ) e. CC )
3	2	ancoms	|- ( ( A e. ~H /\ x e. ~H ) -> ( x .ih A ) e. CC )
4	1 3	fmpt3d	|- ( A e. ~H -> ( bra ` A ) : ~H --> CC )