eldm1cossres

Description: Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018)

		Ref	Expression
	Assertion	eldm1cossres	$⊢ B \in V \to (B \in dom ≀ ({R ↾}_{A}) \leftrightarrow \exists u \in A u R B)$

Step	Hyp	Ref	Expression
1		eldmcoss	$⊢ B \in V \to (B \in dom ≀ ({R ↾}_{A}) \leftrightarrow \exists u u ({R ↾}_{A}) B)$
2		brres	$⊢ B \in V \to (u ({R ↾}_{A}) B \leftrightarrow (u \in A \land u R B))$
3	2	exbidv	$⊢ B \in V \to (\exists u u ({R ↾}_{A}) B \leftrightarrow \exists u (u \in A \land u R B))$
4	1 3	bitrd	$⊢ B \in V \to (B \in dom ≀ ({R ↾}_{A}) \leftrightarrow \exists u (u \in A \land u R B))$
5		df-rex	$⊢ \exists u \in A u R B \leftrightarrow \exists u (u \in A \land u R B)$
6	4 5	bitr4di	$⊢ B \in V \to (B \in dom ≀ ({R ↾}_{A}) \leftrightarrow \exists u \in A u R B)$

Metamath Proof Explorer