Metamath Proof Explorer


Theorem cnvbrabra

Description: The converse bra of the bra of a vector is the vector itself. (Contributed by NM, 30-May-2006) (New usage is discouraged.)

Ref Expression
Assertion cnvbrabra Abra-1braA=A

Proof

Step Hyp Ref Expression
1 bra11 bra:1-1 ontoLinFnContFn
2 f1ocnvfv1 bra:1-1 ontoLinFnContFnAbra-1braA=A
3 1 2 mpan Abra-1braA=A