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

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

Proof of Theorem resmpt2
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 resoprab2 6754 . 2 ((𝐶𝐴𝐷𝐵) → ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐸)} ↾ (𝐶 × 𝐷)) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐶𝑦𝐷) ∧ 𝑧 = 𝐸)})
2 df-mpt2 6652 . . 3 (𝑥𝐴, 𝑦𝐵𝐸) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐸)}
32reseq1i 5390 . 2 ((𝑥𝐴, 𝑦𝐵𝐸) ↾ (𝐶 × 𝐷)) = ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐸)} ↾ (𝐶 × 𝐷))
4 df-mpt2 6652 . 2 (𝑥𝐶, 𝑦𝐷𝐸) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐶𝑦𝐷) ∧ 𝑧 = 𝐸)}
51, 3, 43eqtr4g 2680 1 ((𝐶𝐴𝐷𝐵) → ((𝑥𝐴, 𝑦𝐵𝐸) ↾ (𝐶 × 𝐷)) = (𝑥𝐶, 𝑦𝐷𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1482  wcel 1989  wss 3572   × cxp 5110  cres 5114  {coprab 6648  cmpt2 6649
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pr 4904
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-opab 4711  df-xp 5118  df-rel 5119  df-res 5124  df-oprab 6651  df-mpt2 6652
This theorem is referenced by:  ofmres  7161  cantnfval2  8563  pgrpsubgsymg  17822  sylow3lem5  18040  phssip  19997  mamures  20190  mdetrsca2  20404  mdetrlin2  20407  mdetunilem5  20416  smadiadetglem1  20471  smadiadetglem2  20472  pmatcollpw3lem  20582  txss12  21402  txbasval  21403  cnmpt2res  21474  fmucndlem  22089  cnmpt2pc  22721  oprpiece1res1  22744  oprpiece1res2  22745  cxpcn3  24483  ressplusf  29635  submatres  29857  cvmlift2lem6  31275  cvmlift2lem12  31281  icorempt2  33179  elicores  39569  volicorescl  40536  rngchomrnghmresALTV  41767  rhmsubclem1  41857  rhmsubcALTVlem1  41875
  Copyright terms: Public domain W3C validator