Theorem cosscnvelrels

Description: Cosets of converse sets are elements of the relations class. (Contributed by Peter Mazsa, 31-Aug-2021)

	Ref	Expression
Assertion	cosscnvelrels	⊢ ( 𝐴 ∈ 𝑉 → ≀ ◡ 𝐴 ∈ Rels )

Proof

Step	Hyp	Ref	Expression
1		cnvelrels	⊢ ( 𝐴 ∈ 𝑉 → ◡ 𝐴 ∈ Rels )
2		cosselrels	⊢ ( ◡ 𝐴 ∈ Rels → ≀ ◡ 𝐴 ∈ Rels )
3	1 2	syl	⊢ ( 𝐴 ∈ 𝑉 → ≀ ◡ 𝐴 ∈ Rels )