ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dmres GIF version

Theorem dmres 4890
Description: The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
dmres dom (𝐴𝐵) = (𝐵 ∩ dom 𝐴)

Proof of Theorem dmres
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2715 . . . . 5 𝑥 ∈ V
21eldm2 4787 . . . 4 (𝑥 ∈ dom (𝐴𝐵) ↔ ∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵))
3 19.41v 1882 . . . . 5 (∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵) ↔ (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
4 vex 2715 . . . . . . 7 𝑦 ∈ V
54opelres 4874 . . . . . 6 (⟨𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
65exbii 1585 . . . . 5 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ ∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
71eldm2 4787 . . . . . 6 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
87anbi1i 454 . . . . 5 ((𝑥 ∈ dom 𝐴𝑥𝐵) ↔ (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
93, 6, 83bitr4i 211 . . . 4 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (𝑥 ∈ dom 𝐴𝑥𝐵))
102, 9bitr2i 184 . . 3 ((𝑥 ∈ dom 𝐴𝑥𝐵) ↔ 𝑥 ∈ dom (𝐴𝐵))
1110ineqri 3301 . 2 (dom 𝐴𝐵) = dom (𝐴𝐵)
12 incom 3300 . 2 (dom 𝐴𝐵) = (𝐵 ∩ dom 𝐴)
1311, 12eqtr3i 2180 1 dom (𝐴𝐵) = (𝐵 ∩ dom 𝐴)
Colors of variables: wff set class
Syntax hints:  wa 103   = wceq 1335  wex 1472  wcel 2128  cin 3101  cop 3564  dom cdm 4589  cres 4591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4085  ax-pow 4138  ax-pr 4172
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3546  df-sn 3567  df-pr 3568  df-op 3570  df-br 3968  df-opab 4029  df-xp 4595  df-dm 4599  df-res 4601
This theorem is referenced by:  ssdmres  4891  dmresexg  4892  imadisj  4951  ndmima  4966  imainrect  5034  dmresv  5047  resdmres  5080  funimacnv  5249  fnresdisj  5283  fnres  5289  ssimaex  5532  fnreseql  5580  respreima  5598  ffvresb  5633  fsnunfv  5671  funfvima  5701  offres  6086  smores  6242  smores3  6243  smores2  6244  fnfi  6884  sbthlemi5  6908  sbthlem7  6910  dmaddpi  7248  dmmulpi  7249  fvsetsid  12320  setsfun  12321  setsfun0  12322  setsresg  12324  lmres  12744  metreslem  12876
  Copyright terms: Public domain W3C validator