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 3991 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 5776 | . 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
7 | 1 | cv 1330 | . . . . . 6 class 𝑥 |
8 | 7, 3 | wcel 1480 | . . . . 5 wff 𝑥 ∈ 𝐴 |
9 | 2 | cv 1330 | . . . . . 6 class 𝑦 |
10 | 9, 4 | wcel 1480 | . . . . 5 wff 𝑦 ∈ 𝐵 |
11 | 8, 10 | wa 103 | . . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
12 | vz | . . . . . 6 setvar 𝑧 | |
13 | 12 | cv 1330 | . . . . 5 class 𝑧 |
14 | 13, 5 | wceq 1331 | . . . 4 wff 𝑧 = 𝐶 |
15 | 11, 14 | wa 103 | . . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) |
16 | 15, 1, 2, 12 | coprab 5775 | . 2 class {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
17 | 6, 16 | wceq 1331 | 1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
Colors of variables: wff set class |
This definition is referenced by: mpoeq123 5830 mpoeq123dva 5832 mpoeq3dva 5835 nfmpo1 5838 nfmpo2 5839 nfmpo 5840 mpo0 5841 cbvmpox 5849 mpov 5861 mpomptx 5862 resmpo 5869 mpofun 5873 mpo2eqb 5880 rnmpo 5881 reldmmpo 5882 ovmpt4g 5893 elmpocl 5968 fmpox 6098 f1od2 6132 tposmpo 6178 erovlem 6521 xpcomco 6720 dfplpq2 7162 dfmpq2 7163 |
Copyright terms: Public domain | W3C validator |