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 3959 | . 2 class (𝑥 ∈ 𝐴 ↦ 𝐵) |
5 | 1 | cv 1315 | . . . . 5 class 𝑥 |
6 | 5, 2 | wcel 1465 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1315 | . . . . 5 class 𝑦 |
9 | 8, 3 | wceq 1316 | . . . 4 wff 𝑦 = 𝐵 |
10 | 6, 9 | wa 103 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) |
11 | 10, 1, 7 | copab 3958 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
12 | 4, 11 | wceq 1316 | 1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
Colors of variables: wff set class |
This definition is referenced by: mpteq12f 3978 nfmpt 3990 nfmpt1 3991 cbvmptf 3992 cbvmpt 3993 mptv 3995 fconstmpt 4556 mptrel 4637 rnmpt 4757 resmpt 4837 mptresid 4843 mptcnv 4911 mptpreima 5002 funmpt 5131 dfmpt3 5215 mptfng 5218 mptun 5224 dffn5im 5435 fvmptss2 5464 fvmptg 5465 fndmin 5495 f1ompt 5539 fmptco 5554 mpomptx 5830 f1ocnvd 5940 f1od2 6100 dftpos4 6128 mapsncnv 6557 |
Copyright terms: Public domain | W3C validator |