relssresb

Description: Biconditional form of relssres , to replace it. (Contributed by BJ, 8-Nov-2026)

		Ref	Expression
	Assertion	relssresb	$⊢ (Rel A \land dom A \subseteq B) \leftrightarrow {A ↾}_{B} = A$

Step	Hyp	Ref	Expression
1		relssdmrnb	$⊢ Rel A \leftrightarrow A \subseteq dom A \times ran A$
2		simpl	$⊢ (A \subseteq dom A \times ran A \land dom A \subseteq B) \to A \subseteq dom A \times ran A$
3		simpr	$⊢ (A \subseteq dom A \times ran A \land dom A \subseteq B) \to dom A \subseteq B$
4		ssv	$⊢ ran A \subseteq V$
5		xpss12	$⊢ (dom A \subseteq B \land ran A \subseteq V) \to dom A \times ran A \subseteq B \times V$
6	3 4 5	sylancl	$⊢ (A \subseteq dom A \times ran A \land dom A \subseteq B) \to dom A \times ran A \subseteq B \times V$
7	2 6	sstrd	$⊢ (A \subseteq dom A \times ran A \land dom A \subseteq B) \to A \subseteq B \times V$
8	1 7	sylanb	$⊢ (Rel A \land dom A \subseteq B) \to A \subseteq B \times V$
9		id	$⊢ A \subseteq B \times V \to A \subseteq B \times V$
10		xpss	$⊢ B \times V \subseteq V \times V$
11	9 10	sstrdi	$⊢ A \subseteq B \times V \to A \subseteq V \times V$
12		df-rel	$⊢ Rel A \leftrightarrow A \subseteq V \times V$
13	11 12	sylibr	$⊢ A \subseteq B \times V \to Rel A$
14		dmss	$⊢ A \subseteq B \times V \to dom A \subseteq dom (B \times V)$
15		dmxpss	$⊢ dom (B \times V) \subseteq B$
16	14 15	sstrdi	$⊢ A \subseteq B \times V \to dom A \subseteq B$
17	13 16	jca	$⊢ A \subseteq B \times V \to (Rel A \land dom A \subseteq B)$
18	8 17	impbii	$⊢ (Rel A \land dom A \subseteq B) \leftrightarrow A \subseteq B \times V$
19		bj-resssxp	$⊢ {A ↾}_{B} = A \leftrightarrow A \subseteq B \times V$
20	18 19	bitr4i	$⊢ (Rel A \land dom A \subseteq B) \leftrightarrow {A ↾}_{B} = A$

Metamath Proof Explorer