Theorem xrnrel

Description: A range Cartesian product is a relation. This is Scott Fenton's txprel with a different symbol, see https://github.com/metamath/set.mm/issues/2469 . (Contributed by Scott Fenton, 31-Mar-2012)

	Ref	Expression
Assertion	xrnrel	⊢ Rel ( 𝐴 ⋉ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		xrnss3v	⊢ ( 𝐴 ⋉ 𝐵 ) ⊆ ( V × ( V × V ) )
2		xpss	⊢ ( V × ( V × V ) ) ⊆ ( V × V )
3	1 2	sstri	⊢ ( 𝐴 ⋉ 𝐵 ) ⊆ ( V × V )
4		df-rel	⊢ ( Rel ( 𝐴 ⋉ 𝐵 ) ↔ ( 𝐴 ⋉ 𝐵 ) ⊆ ( V × V ) )
5	3 4	mpbir	⊢ Rel ( 𝐴 ⋉ 𝐵 )