Theorem resmpo 7509

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.

Step	Hyp	Ref	Expression
1		resoprab2 7508	. 2 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐸)} ↾ (𝐶 × 𝐷)) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐸)})
2		df-mpo 7392	. . 3 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐸)}
3	2	reseq1i 5946	. 2 ⊢ ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) ↾ (𝐶 × 𝐷)) = ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐸)} ↾ (𝐶 × 𝐷))
4		df-mpo 7392	. 2 ⊢ (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐸)}
5	1, 3, 4	3eqtr4g 2789	1 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) ↾ (𝐶 × 𝐷)) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ⊆ wss 3914   × cxp 5636   ↾ cres 5640  {coprab 7388   ∈ cmpo 7389

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5170  df-xp 5644  df-rel 5645  df-res 5650  df-oprab 7391  df-mpo 7392

This theorem is referenced by:  elimampo  7526  ofmres  7963  cantnfval2  9622  submefmnd  18822  pgrpsubgsymg  19339  sylow3lem5  19561  rhmsubclem1  20594  phssip  21567  mamures  22284  mdetrsca2  22491  mdetrlin2  22494  mdetunilem5  22503  smadiadetglem1  22558  smadiadetglem2  22559  pmatcollpw3lem  22670  txss12  23492  txbasval  23493  cnmpt2res  23564  fmucndlem  24178  cnmpopc  24822  oprpiece1res1  24849  oprpiece1res2  24850  cxpcn3  26658  ressplusf  32885  submatres  33796  cvmlift2lem6  35295  cvmlift2lem12  35301  icorempo  37339  elicores  45531  volicorescl  46551  rngchomrnghmresALTV  48264  rhmsubcALTVlem1  48266  rescofuf  49079