1cossres

Description: The class of cosets by a restriction. (Contributed by Peter Mazsa, 20-Apr-2019)

		Ref	Expression
	Assertion	1cossres	$⊢ ≀ ({R ↾}_{A}) = \{⟨x, y⟩ \| \exists u \in A (u R x \land u R y)\}$

Step	Hyp	Ref	Expression
1		df-coss	$⊢ ≀ ({R ↾}_{A}) = \{⟨x, y⟩ \| \exists u (u ({R ↾}_{A}) x \land u ({R ↾}_{A}) y)\}$
2		df-rex	$⊢ \exists u \in A (u R x \land u R y) \leftrightarrow \exists u (u \in A \land (u R x \land u R y))$
3		anandi	$⊢ (u \in A \land (u R x \land u R y)) \leftrightarrow ((u \in A \land u R x) \land (u \in A \land u R y))$
4		brres	$⊢ x \in V \to (u ({R ↾}_{A}) x \leftrightarrow (u \in A \land u R x))$
5	4	elv	$⊢ u ({R ↾}_{A}) x \leftrightarrow (u \in A \land u R x)$
6		brres	$⊢ y \in V \to (u ({R ↾}_{A}) y \leftrightarrow (u \in A \land u R y))$
7	6	elv	$⊢ u ({R ↾}_{A}) y \leftrightarrow (u \in A \land u R y)$
8	5 7	anbi12i	$⊢ (u ({R ↾}_{A}) x \land u ({R ↾}_{A}) y) \leftrightarrow ((u \in A \land u R x) \land (u \in A \land u R y))$
9	3 8	bitr4i	$⊢ (u \in A \land (u R x \land u R y)) \leftrightarrow (u ({R ↾}_{A}) x \land u ({R ↾}_{A}) y)$
10	9	exbii	$⊢ \exists u (u \in A \land (u R x \land u R y)) \leftrightarrow \exists u (u ({R ↾}_{A}) x \land u ({R ↾}_{A}) y)$
11	2 10	bitri	$⊢ \exists u \in A (u R x \land u R y) \leftrightarrow \exists u (u ({R ↾}_{A}) x \land u ({R ↾}_{A}) y)$
12	11	opabbii	$⊢ \{⟨x, y⟩ \| \exists u \in A (u R x \land u R y)\} = \{⟨x, y⟩ \| \exists u (u ({R ↾}_{A}) x \land u ({R ↾}_{A}) y)\}$
13	1 12	eqtr4i	$⊢ ≀ ({R ↾}_{A}) = \{⟨x, y⟩ \| \exists u \in A (u R x \land u R y)\}$

Metamath Proof Explorer