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

Metamath Proof Explorer

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 )