Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > resmpt2 | Structured version Visualization version GIF version |
Description: Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.) |
Ref | Expression |
---|---|
resmpt2 | ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) ↾ (𝐶 × 𝐷)) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resoprab2 6757 | . 2 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐸)} ↾ (𝐶 × 𝐷)) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐸)}) | |
2 | df-mpt2 6655 | . . 3 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐸)} | |
3 | 2 | reseq1i 5392 | . 2 ⊢ ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) ↾ (𝐶 × 𝐷)) = ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐸)} ↾ (𝐶 × 𝐷)) |
4 | df-mpt2 6655 | . 2 ⊢ (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐸)} | |
5 | 1, 3, 4 | 3eqtr4g 2681 | 1 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) ↾ (𝐶 × 𝐷)) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ⊆ wss 3574 × cxp 5112 ↾ cres 5116 {coprab 6651 ↦ cmpt2 6652 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-opab 4713 df-xp 5120 df-rel 5121 df-res 5126 df-oprab 6654 df-mpt2 6655 |
This theorem is referenced by: ofmres 7164 cantnfval2 8566 pgrpsubgsymg 17828 sylow3lem5 18046 phssip 20003 mamures 20196 mdetrsca2 20410 mdetrlin2 20413 mdetunilem5 20422 smadiadetglem1 20477 smadiadetglem2 20478 pmatcollpw3lem 20588 txss12 21408 txbasval 21409 cnmpt2res 21480 fmucndlem 22095 cnmpt2pc 22727 oprpiece1res1 22750 oprpiece1res2 22751 cxpcn3 24489 ressplusf 29650 submatres 29872 cvmlift2lem6 31290 cvmlift2lem12 31296 icorempt2 33199 elicores 39760 volicorescl 40767 rngchomrnghmresALTV 41996 rhmsubclem1 42086 rhmsubcALTVlem1 42104 |
Copyright terms: Public domain | W3C validator |