![]() |
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 3921 | . 2 class (𝑥 ∈ 𝐴 ↦ 𝐵) |
5 | 1 | cv 1295 | . . . . 5 class 𝑥 |
6 | 5, 2 | wcel 1445 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1295 | . . . . 5 class 𝑦 |
9 | 8, 3 | wceq 1296 | . . . 4 wff 𝑦 = 𝐵 |
10 | 6, 9 | wa 103 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) |
11 | 10, 1, 7 | copab 3920 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
12 | 4, 11 | wceq 1296 | 1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
Colors of variables: wff set class |
This definition is referenced by: mpteq12f 3940 nfmpt 3952 nfmpt1 3953 cbvmptf 3954 cbvmpt 3955 mptv 3957 fconstmpt 4514 mptrel 4595 rnmpt 4715 resmpt 4793 mptresid 4799 mptcnv 4867 mptpreima 4958 funmpt 5086 dfmpt3 5170 mptfng 5173 mptun 5178 dffn5im 5385 fvmptss2 5414 fvmptg 5415 fndmin 5445 f1ompt 5489 fmptco 5503 mpt2mptx 5777 f1ocnvd 5884 f1od2 6038 dftpos4 6066 mapsncnv 6492 |
Copyright terms: Public domain | W3C validator |