Theorem relssres 6015

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 488	. . . 4 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → Rel 𝐴)
2		vex 3454	. . . . . . . . 9 ⊢ 𝑥 ∈ V
3		vex 3454	. . . . . . . . 9 ⊢ 𝑦 ∈ V
4	2, 3	opeldm 5891	. . . . . . . 8 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → 𝑥 ∈ dom 𝐴)
5		ssel 3925	. . . . . . . 8 ⊢ (dom 𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ 𝐵))
6	4, 5	syl5 35	. . . . . . 7 ⊢ (dom 𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → 𝑥 ∈ 𝐵))
7	6	ancrd 561	. . . . . 6 ⊢ (dom 𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)))
8	3	opelresi 5980	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	7, 8	imbitrrdi 255	. . . . 5 ⊢ (dom 𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵)))
10	9	adantl 487	. . . 4 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵)))
11	1, 10	relssdv 5768	. . 3 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → 𝐴 ⊆ (𝐴 ↾ 𝐵))
12		resss 5994	. . 3 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴
13	11, 12	jctil 529	. 2 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → ((𝐴 ↾ 𝐵) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐴 ↾ 𝐵)))
14		eqss 3946	. 2 ⊢ ((𝐴 ↾ 𝐵) = 𝐴 ↔ ((𝐴 ↾ 𝐵) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐴 ↾ 𝐵)))
15	13, 14	sylibr 237	1 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → (𝐴 ↾ 𝐵) = 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ⊆ wss 3899  ⟨cop 4590  dom cdm 5655   ↾ cres 5657  Rel wrel 5660

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5661  df-rel 5662  df-dm 5665  df-res 5667

This theorem is used by:  resdm  6019  relresfld  6273  fnresdm  6652  focofo  6803  f1ompt  7105  tfr2b  8386  tz7.48-2  8432  omxpenlem  9077  pwfir  9287  rankwflemb  9776  zorn2lem4  10502  relexpaddg  15127  setscom  17273  setsid  17300  dprd2da  20172  dprd2db  20173  ustssco  24442  dvres3  26141  dvres3a  26142  rlimcnp2  27204  nolt02o  27932  nogt01o  27933  nosupbnd1  27951  noinfbnd1  27966  ex-res  30922  symgcom2  33525  fineqvnttrclse  35651  poimirlem3  38373  relexpaddss  44559  fnresdmss  46001  limsupresuz  46532  liminfresuz  46613  isubgrvtxuhgr  48781  tposresg  49805