![]() |
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 3997 | . 2 class (𝑥 ∈ 𝐴 ↦ 𝐵) |
5 | 1 | cv 1331 | . . . . 5 class 𝑥 |
6 | 5, 2 | wcel 1481 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1331 | . . . . 5 class 𝑦 |
9 | 8, 3 | wceq 1332 | . . . 4 wff 𝑦 = 𝐵 |
10 | 6, 9 | wa 103 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) |
11 | 10, 1, 7 | copab 3996 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
12 | 4, 11 | wceq 1332 | 1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
Colors of variables: wff set class |
This definition is referenced by: mpteq12f 4016 nfmpt 4028 nfmpt1 4029 cbvmptf 4030 cbvmpt 4031 mptv 4033 fconstmpt 4594 mptrel 4675 rnmpt 4795 resmpt 4875 mptresid 4881 mptcnv 4949 mptpreima 5040 funmpt 5169 dfmpt3 5253 mptfng 5256 mptun 5262 dffn5im 5475 fvmptss2 5504 fvmptg 5505 fndmin 5535 f1ompt 5579 fmptco 5594 mpomptx 5870 f1ocnvd 5980 f1od2 6140 dftpos4 6168 mapsncnv 6597 |
Copyright terms: Public domain | W3C validator |