Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-mpt2 | Structured version Visualization version GIF version |
Description: Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from 𝑥, 𝑦 (in 𝐴 × 𝐵) to 𝐶(𝑥, 𝑦)." An extension of df-mpt 4645 for two arguments. (Contributed by NM, 17-Feb-2008.) |
Ref | Expression |
---|---|
df-mpt2 | ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . 3 setvar 𝑥 | |
2 | vy | . . 3 setvar 𝑦 | |
3 | cA | . . 3 class 𝐴 | |
4 | cB | . . 3 class 𝐵 | |
5 | cC | . . 3 class 𝐶 | |
6 | 1, 2, 3, 4, 5 | cmpt2 6551 | . 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
7 | 1 | cv 1474 | . . . . . 6 class 𝑥 |
8 | 7, 3 | wcel 1977 | . . . . 5 wff 𝑥 ∈ 𝐴 |
9 | 2 | cv 1474 | . . . . . 6 class 𝑦 |
10 | 9, 4 | wcel 1977 | . . . . 5 wff 𝑦 ∈ 𝐵 |
11 | 8, 10 | wa 383 | . . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
12 | vz | . . . . . 6 setvar 𝑧 | |
13 | 12 | cv 1474 | . . . . 5 class 𝑧 |
14 | 13, 5 | wceq 1475 | . . . 4 wff 𝑧 = 𝐶 |
15 | 11, 14 | wa 383 | . . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) |
16 | 15, 1, 2, 12 | coprab 6550 | . 2 class {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
17 | 6, 16 | wceq 1475 | 1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
Colors of variables: wff setvar class |
This definition is referenced by: mpt2eq123 6612 mpt2eq123dva 6614 mpt2eq3dva 6617 nfmpt21 6620 nfmpt22 6621 nfmpt2 6622 mpt20 6623 cbvmpt2x 6631 mpt2v 6648 mpt2mptx 6649 resmpt2 6656 mpt2fun 6660 mpt22eqb 6667 rnmpt2 6668 reldmmpt2 6669 elrnmpt2res 6672 ovmpt4g 6681 mpt2ndm0 6773 elmpt2cl 6774 fmpt2x 7125 bropopvvv 7142 bropfvvvv 7144 tposmpt2 7276 erovlem 7730 xpcomco 7935 omxpenlem 7946 cpnnen 14797 2wlkonot3v 26402 2spthonot3v 26403 mpt2mptxf 28860 df1stres 28864 df2ndres 28865 f1od2 28887 sxbrsigalem5 29677 bj-dfmpt2a 32252 csbmpt22g 32353 uncf 32558 unccur 32562 mpt2bi123f 33141 cbvmpt22 38305 cbvmpt21 38306 mpt2mptx2 41906 cbvmpt2x2 41907 |
Copyright terms: Public domain | W3C validator |