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 4045 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 5844 | . 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
7 | 1 | cv 1342 | . . . . . 6 class 𝑥 |
8 | 7, 3 | wcel 2136 | . . . . 5 wff 𝑥 ∈ 𝐴 |
9 | 2 | cv 1342 | . . . . . 6 class 𝑦 |
10 | 9, 4 | wcel 2136 | . . . . 5 wff 𝑦 ∈ 𝐵 |
11 | 8, 10 | wa 103 | . . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
12 | vz | . . . . . 6 setvar 𝑧 | |
13 | 12 | cv 1342 | . . . . 5 class 𝑧 |
14 | 13, 5 | wceq 1343 | . . . 4 wff 𝑧 = 𝐶 |
15 | 11, 14 | wa 103 | . . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) |
16 | 15, 1, 2, 12 | coprab 5843 | . 2 class {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
17 | 6, 16 | wceq 1343 | 1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
Colors of variables: wff set class |
This definition is referenced by: mpoeq123 5901 mpoeq123dva 5903 mpoeq3dva 5906 nfmpo1 5909 nfmpo2 5910 nfmpo 5911 mpo0 5912 cbvmpox 5920 mpov 5932 mpomptx 5933 resmpo 5940 mpofun 5944 mpo2eqb 5951 rnmpo 5952 reldmmpo 5953 ovmpt4g 5964 elmpocl 6036 fmpox 6168 f1od2 6203 tposmpo 6249 erovlem 6593 xpcomco 6792 dfplpq2 7295 dfmpq2 7296 |
Copyright terms: Public domain | W3C validator |