ressn2

Description: A class ' R ' restricted to the singleton of the class ' A ' is the ordered pair class abstraction of the class ' A ' and the sets in relation ' R ' to ' A ' (and not in relation to the singleton ' { A } ' ). (Contributed by Peter Mazsa, 16-Jun-2024)

		Ref	Expression
	Assertion	ressn2	$⊢ {R ↾}_{\{A\}} = \{⟨a, u⟩ \| (a = A \land A R u)\}$

Proof

Step	Hyp	Ref	Expression
1		dfres2	$⊢ {R ↾}_{\{A\}} = \{⟨a, u⟩ \| (a \in \{A\} \land a R u)\}$
2		velsn	$⊢ a \in \{A\} \leftrightarrow a = A$
3	2	anbi1i	$⊢ (a \in \{A\} \land a R u) \leftrightarrow (a = A \land a R u)$
4		eqbrb	$⊢ (a = A \land a R u) \leftrightarrow (a = A \land A R u)$
5	3 4	bitri	$⊢ (a \in \{A\} \land a R u) \leftrightarrow (a = A \land A R u)$
6	5	opabbii	$⊢ \{⟨a, u⟩ \| (a \in \{A\} \land a R u)\} = \{⟨a, u⟩ \| (a = A \land A R u)\}$
7	1 6	eqtri	$⊢ {R ↾}_{\{A\}} = \{⟨a, u⟩ \| (a = A \land A R u)\}$

Metamath Proof Explorer

Theorem ressn2

Proof