eldmressnALTV

Description: Element of the domain of a restriction to a singleton. (Contributed by Peter Mazsa, 12-Jun-2024)

		Ref	Expression
	Assertion	eldmressnALTV	$⊢ B \in V \to (B \in dom ({R ↾}_{\{A\}}) \leftrightarrow (B = A \land A \in dom 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		elsng	$⊢ B \in V \to (B \in \{A\} \leftrightarrow B = A)$
3		eldmg	$⊢ B \in V \to (B \in dom R \leftrightarrow \exists y B R y)$
4	3	bicomd	$⊢ B \in V \to (\exists y B R y \leftrightarrow B \in dom R)$
5	2 4	anbi12d	$⊢ B \in V \to ((B \in \{A\} \land \exists y B R y) \leftrightarrow (B = A \land B \in dom R))$
6	1 5	bitrd	$⊢ B \in V \to (B \in dom ({R ↾}_{\{A\}}) \leftrightarrow (B = A \land B \in dom R))$
7		eqelb	$⊢ (B = A \land B \in dom R) \leftrightarrow (B = A \land A \in dom R)$
8	6 7	bitrdi	$⊢ B \in V \to (B \in dom ({R ↾}_{\{A\}}) \leftrightarrow (B = A \land A \in dom R))$

Metamath Proof Explorer