Metamath Proof Explorer


Theorem symrelcoss3

Description: The class of cosets by R is symmetric, see dfsymrel3 . (Contributed by Peter Mazsa, 28-Mar-2019) (Revised by Peter Mazsa, 17-Sep-2021)

Ref Expression
Assertion symrelcoss3 ( ∀ 𝑥𝑦 ( 𝑥𝑅 𝑦𝑦𝑅 𝑥 ) ∧ Rel ≀ 𝑅 )

Proof

Step Hyp Ref Expression
1 brcosscnvcoss ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥𝑅 𝑦𝑦𝑅 𝑥 ) )
2 1 el2v ( 𝑥𝑅 𝑦𝑦𝑅 𝑥 )
3 2 biimpi ( 𝑥𝑅 𝑦𝑦𝑅 𝑥 )
4 3 gen2 𝑥𝑦 ( 𝑥𝑅 𝑦𝑦𝑅 𝑥 )
5 relcoss Rel ≀ 𝑅
6 4 5 pm3.2i ( ∀ 𝑥𝑦 ( 𝑥𝑅 𝑦𝑦𝑅 𝑥 ) ∧ Rel ≀ 𝑅 )