Theorem relssres 5981

Description: Simplification law for restriction. (Contributed by NM, 16-Aug-1994.)

Assertion

Ref	Expression
relssres	⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → (𝐴 ↾ 𝐵) = 𝐴)

Proof of Theorem relssres

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 482	. . . 4 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → Rel 𝐴)
2		vex 3444	. . . . . . . . 9 ⊢ 𝑥 ∈ V
3		vex 3444	. . . . . . . . 9 ⊢ 𝑦 ∈ V
4	2, 3	opeldm 5856	. . . . . . . 8 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → 𝑥 ∈ dom 𝐴)
5		ssel 3927	. . . . . . . 8 ⊢ (dom 𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ 𝐵))
6	4, 5	syl5 34	. . . . . . 7 ⊢ (dom 𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → 𝑥 ∈ 𝐵))
7	6	ancrd 551	. . . . . 6 ⊢ (dom 𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)))
8	3	opelresi 5946	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	7, 8	imbitrrdi 252	. . . . 5 ⊢ (dom 𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵)))
10	9	adantl 481	. . . 4 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵)))
11	1, 10	relssdv 5737	. . 3 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → 𝐴 ⊆ (𝐴 ↾ 𝐵))
12		resss 5960	. . 3 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴
13	11, 12	jctil 519	. 2 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → ((𝐴 ↾ 𝐵) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐴 ↾ 𝐵)))
14		eqss 3949	. 2 ⊢ ((𝐴 ↾ 𝐵) = 𝐴 ↔ ((𝐴 ↾ 𝐵) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐴 ↾ 𝐵)))
15	13, 14	sylibr 234	1 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → (𝐴 ↾ 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ⊆ wss 3901  ⟨cop 4586  dom cdm 5624   ↾ cres 5626  Rel wrel 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-rel 5631  df-dm 5634  df-res 5636

This theorem is referenced by:  resdm  5985  fnresdm  6611  focofo  6759  f1ompt  7056  tfr2b  8327  tz7.48-2  8373  omxpenlem  9006  pwfir  9217  rankwflemb  9705  zorn2lem4  10409  relexpaddg  14976  setscom  17107  setsid  17134  dprd2da  19973  dprd2db  19974  ustssco  24159  dvres3  25870  dvres3a  25871  rlimcnp2  26932  nolt02o  27663  nogt01o  27664  nosupbnd1  27682  noinfbnd1  27697  ex-res  30516  symgcom2  33166  fineqvnttrclse  35280  poimirlem3  37824  relexpaddss  43969  fnresdmss  45422  limsupresuz  45957  liminfresuz  46038  isubgrvtxuhgr  48120  tposresg  49133