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

Theorem resmpo 7553
Description: Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.)
Assertion
Ref Expression
resmpo ((𝐶𝐴𝐷𝐵) → ((𝑥𝐴, 𝑦𝐵𝐸) ↾ (𝐶 × 𝐷)) = (𝑥𝐶, 𝑦𝐷𝐸))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦
Allowed substitution hints:   𝐸(𝑥,𝑦)

Proof of Theorem resmpo
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 resoprab2 7552 . 2 ((𝐶𝐴𝐷𝐵) → ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐸)} ↾ (𝐶 × 𝐷)) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐶𝑦𝐷) ∧ 𝑧 = 𝐸)})
2 df-mpo 7436 . . 3 (𝑥𝐴, 𝑦𝐵𝐸) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐸)}
32reseq1i 5993 . 2 ((𝑥𝐴, 𝑦𝐵𝐸) ↾ (𝐶 × 𝐷)) = ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐸)} ↾ (𝐶 × 𝐷))
4 df-mpo 7436 . 2 (𝑥𝐶, 𝑦𝐷𝐸) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐶𝑦𝐷) ∧ 𝑧 = 𝐸)}
51, 3, 43eqtr4g 2802 1 ((𝐶𝐴𝐷𝐵) → ((𝑥𝐴, 𝑦𝐵𝐸) ↾ (𝐶 × 𝐷)) = (𝑥𝐶, 𝑦𝐷𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  wss 3951   × cxp 5683  cres 5687  {coprab 7432  cmpo 7433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-opab 5206  df-xp 5691  df-rel 5692  df-res 5697  df-oprab 7435  df-mpo 7436
This theorem is referenced by:  elimampo  7570  ofmres  8009  cantnfval2  9709  submefmnd  18908  pgrpsubgsymg  19427  sylow3lem5  19649  rhmsubclem1  20685  phssip  21676  mamures  22401  mdetrsca2  22610  mdetrlin2  22613  mdetunilem5  22622  smadiadetglem1  22677  smadiadetglem2  22678  pmatcollpw3lem  22789  txss12  23613  txbasval  23614  cnmpt2res  23685  fmucndlem  24300  cnmpopc  24955  oprpiece1res1  24982  oprpiece1res2  24983  cxpcn3  26791  ressplusf  32948  submatres  33805  cvmlift2lem6  35313  cvmlift2lem12  35319  icorempo  37352  elicores  45546  volicorescl  46568  rngchomrnghmresALTV  48195  rhmsubcALTVlem1  48197  rescofuf  48922
  Copyright terms: Public domain W3C validator