Theorem resmpo 7530

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 7529	. 2 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐸)} ↾ (𝐶 × 𝐷)) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐸)})
2		df-mpo 7415	. . 3 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐸)}
3	2	reseq1i 5974	. 2 ⊢ ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) ↾ (𝐶 × 𝐷)) = ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐸)} ↾ (𝐶 × 𝐷))
4		df-mpo 7415	. 2 ⊢ (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐸)}
5	1, 3, 4	3eqtr4g 2823	1 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) ↾ (𝐶 × 𝐷)) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ⊆ wss 3905   × cxp 5659   ↾ cres 5663  {coprab 7411   ∈ cmpo 7412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5174  df-xp 5667  df-rel 5668  df-res 5673  df-oprab 7414  df-mpo 7415

This theorem is referenced by:  elimampo  7547  ofmres  7977  cantnfval2  9634  submefmnd  18949  pgrpsubgsymg  19474  sylow3lem5  19696  rhmsubclem1  20784  phssip  21808  mamures  22554  mdetrsca2  22761  mdetrlin2  22764  mdetunilem5  22773  smadiadetglem1  22828  smadiadetglem2  22829  pmatcollpw3lem  22940  txss12  23762  txbasval  23763  cnmpt2res  23834  fmucndlem  24447  cnmpopc  25087  oprpiece1res1  25110  oprpiece1res2  25111  cxpcn3  26913  ressplusf  33283  submatres  34196  cvmlift2lem6  35800  cvmlift2lem12  35806  icorempo  37997  elicores  46249  volicorescl  47267  rngchomrnghmresALTV  49044  rhmsubcALTVlem1  49046  rescofuf  49871