![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-mpo | 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 4081 for two arguments. (Contributed by NM, 17-Feb-2008.) |
Ref | Expression |
---|---|
df-mpo | ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
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 | cmpo 5898 | . 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
7 | 1 | cv 1363 | . . . . . 6 class 𝑥 |
8 | 7, 3 | wcel 2160 | . . . . 5 wff 𝑥 ∈ 𝐴 |
9 | 2 | cv 1363 | . . . . . 6 class 𝑦 |
10 | 9, 4 | wcel 2160 | . . . . 5 wff 𝑦 ∈ 𝐵 |
11 | 8, 10 | wa 104 | . . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
12 | vz | . . . . . 6 setvar 𝑧 | |
13 | 12 | cv 1363 | . . . . 5 class 𝑧 |
14 | 13, 5 | wceq 1364 | . . . 4 wff 𝑧 = 𝐶 |
15 | 11, 14 | wa 104 | . . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) |
16 | 15, 1, 2, 12 | coprab 5897 | . 2 class {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
17 | 6, 16 | wceq 1364 | 1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
Colors of variables: wff set class |
This definition is referenced by: mpoeq123 5955 mpoeq123dva 5957 mpoeq3dva 5960 nfmpo1 5963 nfmpo2 5964 nfmpo 5965 mpo0 5966 cbvmpox 5974 mpov 5986 mpomptx 5987 resmpo 5994 mpofun 5998 mpo2eqb 6006 rnmpo 6007 reldmmpo 6008 ovmpt4g 6019 elmpocl 6091 fmpox 6225 f1od2 6260 tposmpo 6306 erovlem 6653 xpcomco 6852 dfplpq2 7383 dfmpq2 7384 |
Copyright terms: Public domain | W3C validator |