brcoss

Description: A and B are cosets by R : a binary relation. (Contributed by Peter Mazsa, 27-Dec-2018)

		Ref	Expression
	Assertion	brcoss	$⊢ (A \in V \land B \in W) \to (A ≀ R B \leftrightarrow \exists u (u R A \land u R B))$

Step	Hyp	Ref	Expression
1		breq2	$⊢ x = A \to (u R x \leftrightarrow u R A)$
2		breq2	$⊢ y = B \to (u R y \leftrightarrow u R B)$
3	1 2	bi2anan9	$⊢ (x = A \land y = B) \to ((u R x \land u R y) \leftrightarrow (u R A \land u R B))$
4	3	exbidv	$⊢ (x = A \land y = B) \to (\exists u (u R x \land u R y) \leftrightarrow \exists u (u R A \land u R B))$
5		df-coss	$⊢ ≀ R = \{⟨x, y⟩ \| \exists u (u R x \land u R y)\}$
6	4 5	brabga	$⊢ (A \in V \land B \in W) \to (A ≀ R B \leftrightarrow \exists u (u R A \land u R B))$

Metamath Proof Explorer