![]() |
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 3949 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 5728 | . 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
7 | 1 | cv 1311 | . . . . . 6 class 𝑥 |
8 | 7, 3 | wcel 1461 | . . . . 5 wff 𝑥 ∈ 𝐴 |
9 | 2 | cv 1311 | . . . . . 6 class 𝑦 |
10 | 9, 4 | wcel 1461 | . . . . 5 wff 𝑦 ∈ 𝐵 |
11 | 8, 10 | wa 103 | . . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
12 | vz | . . . . . 6 setvar 𝑧 | |
13 | 12 | cv 1311 | . . . . 5 class 𝑧 |
14 | 13, 5 | wceq 1312 | . . . 4 wff 𝑧 = 𝐶 |
15 | 11, 14 | wa 103 | . . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) |
16 | 15, 1, 2, 12 | coprab 5727 | . 2 class {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
17 | 6, 16 | wceq 1312 | 1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
Colors of variables: wff set class |
This definition is referenced by: mpoeq123 5782 mpoeq123dva 5784 mpoeq3dva 5787 nfmpo1 5790 nfmpo2 5791 nfmpo 5792 mpo0 5793 cbvmpox 5801 mpov 5813 mpomptx 5814 resmpo 5821 mpofun 5825 mpo2eqb 5832 rnmpo 5833 reldmmpo 5834 ovmpt4g 5845 elmpocl 5920 fmpox 6050 f1od2 6084 tposmpo 6130 erovlem 6473 xpcomco 6671 dfplpq2 7104 dfmpq2 7105 |
Copyright terms: Public domain | W3C validator |