Theorem bnrel

Description: The class of all complex Banach spaces is a relation. (Contributed by NM, 17-Mar-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	bnrel	⊢ Rel CBan

Proof

Step	Hyp	Ref	Expression
1		bnnv	⊢ ( 𝑥 ∈ CBan → 𝑥 ∈ NrmCVec )
2	1	ssriv	⊢ CBan ⊆ NrmCVec
3		nvrel	⊢ Rel NrmCVec
4		relss	⊢ ( CBan ⊆ NrmCVec → ( Rel NrmCVec → Rel CBan ) )
5	2 3 4	mp2	⊢ Rel CBan