Theorem relssresb 38188

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

Assertion

Ref	Expression
relssresb	⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) ↔ (𝐴 ↾ 𝐵) = 𝐴)

Proof of Theorem relssresb

Step	Hyp	Ref	Expression
1		relssdmrnb 38187	. . . 4 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (dom 𝐴 × ran 𝐴))
2		simpl 488	. . . . 5 ⊢ ((𝐴 ⊆ (dom 𝐴 × ran 𝐴) ∧ dom 𝐴 ⊆ 𝐵) → 𝐴 ⊆ (dom 𝐴 × ran 𝐴))
3		simpr 490	. . . . . 6 ⊢ ((𝐴 ⊆ (dom 𝐴 × ran 𝐴) ∧ dom 𝐴 ⊆ 𝐵) → dom 𝐴 ⊆ 𝐵)
4		ssv 3937	. . . . . 6 ⊢ ran 𝐴 ⊆ V
5		xpss12 5671	. . . . . 6 ⊢ ((dom 𝐴 ⊆ 𝐵 ∧ ran 𝐴 ⊆ V) → (dom 𝐴 × ran 𝐴) ⊆ (𝐵 × V))
6	3, 4, 5	sylancl 598	. . . . 5 ⊢ ((𝐴 ⊆ (dom 𝐴 × ran 𝐴) ∧ dom 𝐴 ⊆ 𝐵) → (dom 𝐴 × ran 𝐴) ⊆ (𝐵 × V))
7	2, 6	sstrd 3923	. . . 4 ⊢ ((𝐴 ⊆ (dom 𝐴 × ran 𝐴) ∧ dom 𝐴 ⊆ 𝐵) → 𝐴 ⊆ (𝐵 × V))
8	1, 7	sylanb 593	. . 3 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → 𝐴 ⊆ (𝐵 × V))
9		id 23	. . . . . 6 ⊢ (𝐴 ⊆ (𝐵 × V) → 𝐴 ⊆ (𝐵 × V))
10		xpss 5672	. . . . . 6 ⊢ (𝐵 × V) ⊆ (V × V)
11	9, 10	sstrdi 3925	. . . . 5 ⊢ (𝐴 ⊆ (𝐵 × V) → 𝐴 ⊆ (V × V))
12		df-rel 5663	. . . . 5 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
13	11, 12	sylibr 237	. . . 4 ⊢ (𝐴 ⊆ (𝐵 × V) → Rel 𝐴)
14		dmss 5894	. . . . 5 ⊢ (𝐴 ⊆ (𝐵 × V) → dom 𝐴 ⊆ dom (𝐵 × V))
15		dmxpss 6179	. . . . 5 ⊢ dom (𝐵 × V) ⊆ 𝐵
16	14, 15	sstrdi 3925	. . . 4 ⊢ (𝐴 ⊆ (𝐵 × V) → dom 𝐴 ⊆ 𝐵)
17	13, 16	jca 521	. . 3 ⊢ (𝐴 ⊆ (𝐵 × V) → (Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵))
18	8, 17	impbii 212	. 2 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) ↔ 𝐴 ⊆ (𝐵 × V))
19		bj-resssxp 38176	. 2 ⊢ ((𝐴 ↾ 𝐵) = 𝐴 ↔ 𝐴 ⊆ (𝐵 × V))
20	18, 19	bitr4i 281	1 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) ↔ (𝐴 ↾ 𝐵) = 𝐴)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  Vcvv 3454   ⊆ wss 3900   × cxp 5654  dom cdm 5656  ran crn 5657   ↾ cres 5658  Rel wrel 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-xp 5662  df-rel 5663  df-cnv 5664  df-dm 5666  df-rn 5667  df-res 5668

This theorem is used by:  resdmb  38189