This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in ℋ \land B \in ℋ) \to bra (A) (B) \in ℂ$

Step	Hyp	Ref	Expression
1		brafn	$⊢ A \in ℋ \to bra (A) : ℋ ⟶ ℂ$
2	1	ffvelcdmda	$⊢ (A \in ℋ \land B \in ℋ) \to bra (A) (B) \in ℂ$