Metamath Proof Explorer

Theorem cosscnv

Description: Class of cosets by the converse of R (Contributed by Peter Mazsa, 17-Jun-2020)

Ref Expression
Assertion cosscnv ⊢ ≀ R -1 = x y | ∃ u x R u ∧ y R u

Proof

Step Hyp Ref Expression
1 df-coss ⊢ ≀ R -1 = x y | ∃ u u R -1 x ∧ u R -1 y
2 brcnvg ⊢ u ∈ V ∧ x ∈ V → u R -1 x ↔ x R u
3 2 el2v ⊢ u R -1 x ↔ x R u
4 brcnvg ⊢ u ∈ V ∧ y ∈ V → u R -1 y ↔ y R u
5 4 el2v ⊢ u R -1 y ↔ y R u
6 3 5 anbi12i ⊢ u R -1 x ∧ u R -1 y ↔ x R u ∧ y R u
7 6 exbii ⊢ ∃ u u R -1 x ∧ u R -1 y ↔ ∃ u x R u ∧ y R u
8 7 opabbii ⊢ x y | ∃ u u R -1 x ∧ u R -1 y = x y | ∃ u x R u ∧ y R u
9 1 8 eqtri ⊢ ≀ R -1 = x y | ∃ u x R u ∧ y R u