eldmres2

Description: Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 21-Aug-2020)

		Ref	Expression
	Assertion	eldmres2	$⊢ B \in V \to (B \in dom ({R ↾}_{A}) \leftrightarrow (B \in A \land \exists y y \in [B] R))$

Step	Hyp	Ref	Expression
1		eldmres	$⊢ B \in V \to (B \in dom ({R ↾}_{A}) \leftrightarrow (B \in A \land \exists y B R y))$
2		eldmg	$⊢ B \in V \to (B \in dom R \leftrightarrow \exists y B R y)$
3		eldm4	$⊢ B \in V \to (B \in dom R \leftrightarrow \exists y y \in [B] R)$
4	2 3	bitr3d	$⊢ B \in V \to (\exists y B R y \leftrightarrow \exists y y \in [B] R)$
5	4	anbi2d	$⊢ B \in V \to ((B \in A \land \exists y B R y) \leftrightarrow (B \in A \land \exists y y \in [B] R))$
6	1 5	bitrd	$⊢ B \in V \to (B \in dom ({R ↾}_{A}) \leftrightarrow (B \in A \land \exists y y \in [B] R))$

Metamath Proof Explorer