MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fin Unicode version

Definition df-fin 7540
Description: Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our " ". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 8079. If we accept Infinity, we can also express by (theorem isfinite 8090.) (Contributed by NM, 22-Aug-2008.)
Assertion
Ref Expression
df-fin
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-fin
StepHypRef Expression
1 cfn 7536 . 2
2 vx . . . . . 6
32cv 1394 . . . . 5
4 vy . . . . . 6
54cv 1394 . . . . 5
6 cen 7533 . . . . 5
73, 5, 6wbr 4452 . . . 4
8 com 6700 . . . 4
97, 4, 8wrex 2808 . . 3
109, 2cab 2442 . 2
111, 10wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  isfi  7559  dffin1-5  8789
  Copyright terms: Public domain W3C validator