MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  relssres Structured version   Visualization version   GIF version

Theorem relssres 6022
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.
StepHypRef Expression
1 simpl 483 . . . 4 ((Rel 𝐴 ∧ dom 𝐴𝐵) → Rel 𝐴)
2 vex 3478 . . . . . . . . 9 𝑥 ∈ V
3 vex 3478 . . . . . . . . 9 𝑦 ∈ V
42, 3opeldm 5907 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥 ∈ dom 𝐴)
5 ssel 3975 . . . . . . . 8 (dom 𝐴𝐵 → (𝑥 ∈ dom 𝐴𝑥𝐵))
64, 5syl5 34 . . . . . . 7 (dom 𝐴𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
76ancrd 552 . . . . . 6 (dom 𝐴𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → (𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)))
83opelresi 5989 . . . . . 6 (⟨𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
97, 8imbitrrdi 251 . . . . 5 (dom 𝐴𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ (𝐴𝐵)))
109adantl 482 . . . 4 ((Rel 𝐴 ∧ dom 𝐴𝐵) → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ (𝐴𝐵)))
111, 10relssdv 5788 . . 3 ((Rel 𝐴 ∧ dom 𝐴𝐵) → 𝐴 ⊆ (𝐴𝐵))
12 resss 6006 . . 3 (𝐴𝐵) ⊆ 𝐴
1311, 12jctil 520 . 2 ((Rel 𝐴 ∧ dom 𝐴𝐵) → ((𝐴𝐵) ⊆ 𝐴𝐴 ⊆ (𝐴𝐵)))
14 eqss 3997 . 2 ((𝐴𝐵) = 𝐴 ↔ ((𝐴𝐵) ⊆ 𝐴𝐴 ⊆ (𝐴𝐵)))
1513, 14sylibr 233 1 ((Rel 𝐴 ∧ dom 𝐴𝐵) → (𝐴𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  wss 3948  cop 4634  dom cdm 5676  cres 5678  Rel wrel 5681
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-rel 5683  df-dm 5686  df-res 5688
This theorem is referenced by:  resdm  6026  fnresdm  6669  focofo  6818  f1ompt  7112  tfr2b  8398  tz7.48-2  8444  omxpenlem  9075  pwfir  9178  rankwflemb  9790  zorn2lem4  10496  relexpaddg  15002  setscom  17115  setsid  17143  dprd2da  19914  dprd2db  19915  ustssco  23726  dvres3  25437  dvres3a  25438  rlimcnp2  26478  nolt02o  27205  nogt01o  27206  nosupbnd1  27224  noinfbnd1  27239  ex-res  29732  symgcom2  32286  poimirlem3  36577  relexpaddss  42551  fnresdmss  43946  limsupresuz  44498  liminfresuz  44579
  Copyright terms: Public domain W3C validator