Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pm Structured version   Visualization version   Unicode version

Definition df-pm 7493
 Description: Define the partial mapping operation. A partial function from to is a function from a subset of to . The set of all partial functions from to is written (see pmvalg 7501). A notation for this operation apparently does not appear in the literature. We use to distinguish it from the less general set exponentiation operation (df-map 7492) . See mapsspm 7523 for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007.)
Assertion
Ref Expression
df-pm
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-pm
StepHypRef Expression
1 cpm 7491 . 2
2 vx . . 3
3 vy . . 3
4 cvv 3031 . . 3
5 vf . . . . . 6
65cv 1451 . . . . 5
76wfun 5583 . . . 4
83cv 1451 . . . . . 6
92cv 1451 . . . . . 6
108, 9cxp 4837 . . . . 5
1110cpw 3942 . . . 4
127, 5, 11crab 2760 . . 3
132, 3, 4, 4, 12cmpt2 6310 . 2
141, 13wceq 1452 1
 Colors of variables: wff setvar class This definition is referenced by:  fnpm  7498  pmvalg  7501
 Copyright terms: Public domain W3C validator