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

Definition df-frf 25638
Description: Frechet's filter. Used to define the limit of a sequence. (Contributed by FL, 21-May-2012.)
Assertion
Ref Expression
df-frf  |-  Frf  =  { x  |  E. b ( b  C_  NN  /\  b  e.  Fin  /\  x  =  ( NN 
\  b ) ) }
Distinct variable group:    x, b

Detailed syntax breakdown of Definition df-frf
StepHypRef Expression
1 cfrf 25637 . 2  class  Frf
2 vb . . . . . . 7  set  b
32cv 1622 . . . . . 6  class  b
4 cn 9746 . . . . . 6  class  NN
53, 4wss 3152 . . . . 5  wff  b  C_  NN
6 cfn 6863 . . . . . 6  class  Fin
73, 6wcel 1684 . . . . 5  wff  b  e. 
Fin
8 vx . . . . . . 7  set  x
98cv 1622 . . . . . 6  class  x
104, 3cdif 3149 . . . . . 6  class  ( NN 
\  b )
119, 10wceq 1623 . . . . 5  wff  x  =  ( NN  \  b
)
125, 7, 11w3a 934 . . . 4  wff  ( b 
C_  NN  /\  b  e.  Fin  /\  x  =  ( NN  \  b
) )
1312, 2wex 1528 . . 3  wff  E. b
( b  C_  NN  /\  b  e.  Fin  /\  x  =  ( NN  \  b ) )
1413, 8cab 2269 . 2  class  { x  |  E. b ( b 
C_  NN  /\  b  e.  Fin  /\  x  =  ( NN  \  b
) ) }
151, 14wceq 1623 1  wff  Frf  =  { x  |  E. b ( b  C_  NN  /\  b  e.  Fin  /\  x  =  ( NN 
\  b ) ) }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator