Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-proj Structured version   Unicode version

Definition df-bj-proj 32801
Description: Definition of the class projection corresponding to tagged tuples. The expression  ( A Proj  B
) denotes the projection on the A^th component. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
Assertion
Ref Expression
df-bj-proj  |-  ( A Proj 
B )  =  {
x  |  { x }  e.  ( B " { A } ) }
Distinct variable groups:    x, A    x, B

Detailed syntax breakdown of Definition df-bj-proj
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2bj-cproj 32800 . 2  class  ( A Proj 
B )
4 vx . . . . . 6  setvar  x
54cv 1369 . . . . 5  class  x
65csn 3984 . . . 4  class  { x }
71csn 3984 . . . . 5  class  { A }
82, 7cima 4950 . . . 4  class  ( B
" { A }
)
96, 8wcel 1758 . . 3  wff  { x }  e.  ( B " { A } )
109, 4cab 2439 . 2  class  { x  |  { x }  e.  ( B " { A } ) }
113, 10wceq 1370 1  wff  ( A Proj 
B )  =  {
x  |  { x }  e.  ( B " { A } ) }
Colors of variables: wff setvar class
This definition is referenced by:  bj-projeq  32802  bj-projun  32804  bj-projex  32805  bj-projval  32806
  Copyright terms: Public domain W3C validator