NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-mpt2 Unicode version

Definition df-mpt2 5654
Description: Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from (in ) to ." An extension of df-mpt 5652 for two arguments. (Contributed by SF, 5-Jan-2015.)
Assertion
Ref Expression
df-mpt2
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hints:   (,)   (,)   (,)

Detailed syntax breakdown of Definition df-mpt2
StepHypRef Expression
1 vx . . 3
2 vy . . 3
3 cA . . 3
4 cB . . 3
5 cC . . 3
61, 2, 3, 4, 5cmpt2 5653 . 2
71cv 1641 . . . . . 6
87, 3wcel 1710 . . . . 5
92cv 1641 . . . . . 6
109, 4wcel 1710 . . . . 5
118, 10wa 358 . . . 4
12 vz . . . . . 6
1312cv 1641 . . . . 5
1413, 5wceq 1642 . . . 4
1511, 14wa 358 . . 3
1615, 1, 2, 12coprab 5527 . 2
176, 16wceq 1642 1
Colors of variables: wff setvar class
This definition is referenced by:  mpt2eq123  5661  mpt2eq123dv  5663  mpt2eq3dva  5669  nfmpt21  5673  nfmpt22  5674  nfmpt2  5675  cbvmpt2x  5678  resmpt2  5697  fnov2  5707  mpt2mptx  5708  ovmpt4g  5710  ovmpt2x  5712  ovmpt2ga  5713  rnmpt2  5717  mpt2v  5719  fmpt2x  5730  releqmpt2  5809  composefn  5818  fnce  6176
  Copyright terms: Public domain W3C validator