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

Theorem dmres 4808
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 2661 . . . . 5 𝑥 ∈ V
21eldm2 4705 . . . 4 (𝑥 ∈ dom (𝐴𝐵) ↔ ∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵))
3 19.41v 1856 . . . . 5 (∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵) ↔ (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
4 vex 2661 . . . . . . 7 𝑦 ∈ V
54opelres 4792 . . . . . 6 (⟨𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
65exbii 1567 . . . . 5 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ ∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
71eldm2 4705 . . . . . 6 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
87anbi1i 451 . . . . 5 ((𝑥 ∈ dom 𝐴𝑥𝐵) ↔ (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
93, 6, 83bitr4i 211 . . . 4 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (𝑥 ∈ dom 𝐴𝑥𝐵))
102, 9bitr2i 184 . . 3 ((𝑥 ∈ dom 𝐴𝑥𝐵) ↔ 𝑥 ∈ dom (𝐴𝐵))
1110ineqri 3237 . 2 (dom 𝐴𝐵) = dom (𝐴𝐵)
12 incom 3236 . 2 (dom 𝐴𝐵) = (𝐵 ∩ dom 𝐴)
1311, 12eqtr3i 2138 1 dom (𝐴𝐵) = (𝐵 ∩ dom 𝐴)
Colors of variables: wff set class
Syntax hints:  wa 103   = wceq 1314  wex 1451  wcel 1463  cin 3038  cop 3498  dom cdm 4507  cres 4509
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ral 2396  df-rex 2397  df-v 2660  df-un 3043  df-in 3045  df-ss 3052  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-br 3898  df-opab 3958  df-xp 4513  df-dm 4517  df-res 4519
This theorem is referenced by:  ssdmres  4809  dmresexg  4810  imadisj  4869  ndmima  4884  imainrect  4952  dmresv  4965  resdmres  4998  funimacnv  5167  fnresdisj  5201  fnres  5207  ssimaex  5448  fnreseql  5496  respreima  5514  ffvresb  5549  fsnunfv  5587  funfvima  5615  offres  5999  smores  6155  smores3  6156  smores2  6157  fnfi  6791  sbthlemi5  6815  sbthlem7  6817  dmaddpi  7097  dmmulpi  7098  fvsetsid  11899  setsfun  11900  setsfun0  11901  setsresg  11903  lmres  12323  metreslem  12455
  Copyright terms: Public domain W3C validator