Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-prop Unicode version

Definition df-prop 26042
Description: The set of propositional formulas. Gallier p. 32. (Contributed by FL, 2-Feb-2014.)
Assertion
Ref Expression
df-prop  |-  Prop  =  ( ( ( P c " ( ZZ>= ` 
7 ) )  u. 
{ _|_ c }
)  IndCls  ( { not c ,  and c ,  or s }  u.  { imp c ,  bi c } ) )

Detailed syntax breakdown of Definition df-prop
StepHypRef Expression
1 cprop 26041 . 2  class  Prop
2 cPc 26029 . . . . 5  class  P c
3 c7 9800 . . . . . 6  class  7
4 cuz 10230 . . . . . 6  class  ZZ>=
53, 4cfv 5255 . . . . 5  class  ( ZZ>= ` 
7 )
62, 5cima 4692 . . . 4  class  ( P c " ( ZZ>= ` 
7 ) )
7 cfals 26021 . . . . 5  class  _|_ c
87csn 3640 . . . 4  class  { _|_ c }
96, 8cun 3150 . . 3  class  ( ( P c " ( ZZ>=
`  7 ) )  u.  { _|_ c } )
10 cnotc 26031 . . . . 5  class  not c
11 candc 26033 . . . . 5  class  and c
12 cors 26035 . . . . 5  class  or s
1310, 11, 12ctp 3642 . . . 4  class  { not c ,  and c ,  or s }
14 cimpc 26037 . . . . 5  class  imp c
15 cbic 26039 . . . . 5  class  bi c
1614, 15cpr 3641 . . . 4  class  { imp c ,  bi c }
1713, 16cun 3150 . . 3  class  ( { not c ,  and c ,  or s }  u.  { imp c ,  bi c } )
18 clincl 25993 . . 3  class  IndCls
199, 17, 18co 5858 . 2  class  ( ( ( P c "
( ZZ>= `  7 )
)  u.  { _|_ c } )  IndCls  ( { not c ,  and c ,  or s }  u.  { imp c ,  bi c } ) )
201, 19wceq 1623 1  wff  Prop  =  ( ( ( P c " ( ZZ>= ` 
7 ) )  u. 
{ _|_ c }
)  IndCls  ( { not c ,  and c ,  or s }  u.  { imp c ,  bi c } ) )
Colors of variables: wff set class
This definition is referenced by:  pfsubkl  26047  pvp  26048  pgapspf  26052  pgapspf2  26053
  Copyright terms: Public domain W3C validator