Metamath Proof Explorer

Theorem dfcoss2

Description: Alternate definition of the class of cosets by R : x and y are cosets by R iff there exists a set u such that both x and y are are elements of the R -coset of u (see also the comment of dfec2 ). R is usually a relation. (Contributed by Peter Mazsa, 16-Jan-2018)

Ref Expression
Assertion dfcoss2 ⊢ ≀ R = x y | ∃ u x ∈ u R ∧ y ∈ u R

Proof

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