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⟩ \| \exists u (x \in [u] R \land y \in [u] R)\}$

Proof

Step	Hyp	Ref	Expression
1		df-coss	$⊢ ≀ R = \{⟨x, y⟩ \| \exists u (u R x \land u R y)\}$
2		elecALTV	$⊢ (u \in V \land x \in V) \to (x \in [u] R \leftrightarrow u R x)$
3	2	el2v	$⊢ x \in [u] R \leftrightarrow u R x$
4		elecALTV	$⊢ (u \in V \land y \in V) \to (y \in [u] R \leftrightarrow u R y)$
5	4	el2v	$⊢ y \in [u] R \leftrightarrow u R y$
6	3 5	anbi12i	$⊢ (x \in [u] R \land y \in [u] R) \leftrightarrow (u R x \land u R y)$
7	6	exbii	$⊢ \exists u (x \in [u] R \land y \in [u] R) \leftrightarrow \exists u (u R x \land u R y)$
8	7	opabbii	$⊢ \{⟨x, y⟩ \| \exists u (x \in [u] R \land y \in [u] R)\} = \{⟨x, y⟩ \| \exists u (u R x \land u R y)\}$
9	1 8	eqtr4i	$⊢ ≀ R = \{⟨x, y⟩ \| \exists u (x \in [u] R \land y \in [u] R)\}$

Metamath Proof Explorer

Theorem dfcoss2

Proof