![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-mpt | GIF version |
Description: Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from 𝑥 (in 𝐴) to 𝐵(𝑥)". The class expression 𝐵 is the value of the function at 𝑥 and normally contains the variable 𝑥. Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.) |
Ref | Expression |
---|---|
df-mpt | ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . 3 setvar 𝑥 | |
2 | cA | . . 3 class 𝐴 | |
3 | cB | . . 3 class 𝐵 | |
4 | 1, 2, 3 | cmpt 4079 | . 2 class (𝑥 ∈ 𝐴 ↦ 𝐵) |
5 | 1 | cv 1363 | . . . . 5 class 𝑥 |
6 | 5, 2 | wcel 2160 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1363 | . . . . 5 class 𝑦 |
9 | 8, 3 | wceq 1364 | . . . 4 wff 𝑦 = 𝐵 |
10 | 6, 9 | wa 104 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) |
11 | 10, 1, 7 | copab 4078 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
12 | 4, 11 | wceq 1364 | 1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
Colors of variables: wff set class |
This definition is referenced by: mpteq12f 4098 nfmpt 4110 nfmpt1 4111 cbvmptf 4112 cbvmpt 4113 mptv 4115 fconstmpt 4691 mptrel 4773 rnmpt 4893 resmpt 4973 mptresid 4979 mptcnv 5049 mptpreima 5140 funmpt 5273 dfmpt3 5357 mptfng 5360 mptun 5366 dffn5im 5581 fvmptss2 5611 fvmptg 5612 fndmin 5643 f1ompt 5687 fmptco 5702 mpomptx 5986 f1ocnvd 6095 f1od2 6259 dftpos4 6287 mapsncnv 6720 |
Copyright terms: Public domain | W3C validator |