ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-fin Unicode version

Definition df-fin 6605
Description: Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our " a  e.  Fin". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 13070. (Contributed by NM, 22-Aug-2008.)
Assertion
Ref Expression
df-fin  |-  Fin  =  { x  |  E. y  e.  om  x  ~~  y }
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-fin
StepHypRef Expression
1 cfn 6602 . 2  class  Fin
2 vx . . . . . 6  setvar  x
32cv 1315 . . . . 5  class  x
4 vy . . . . . 6  setvar  y
54cv 1315 . . . . 5  class  y
6 cen 6600 . . . . 5  class  ~~
73, 5, 6wbr 3899 . . . 4  wff  x  ~~  y
8 com 4474 . . . 4  class  om
97, 4, 8wrex 2394 . . 3  wff  E. y  e.  om  x  ~~  y
109, 2cab 2103 . 2  class  { x  |  E. y  e.  om  x  ~~  y }
111, 10wceq 1316 1  wff  Fin  =  { x  |  E. y  e.  om  x  ~~  y }
Colors of variables: wff set class
This definition is referenced by:  isfi  6623
  Copyright terms: Public domain W3C validator