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

Definition df-fin6 8691
Description: A set is VI-finite iff it behaves finitely under X.. Definition VI of [Levy58] p. 4. (Contributed by Stefan O'Rear, 12-Nov-2014.)
Assertion
Ref Expression
df-fin6

Detailed syntax breakdown of Definition df-fin6
StepHypRef Expression
1 cfin6 8684 . 2
2 vx . . . . . 6
32cv 1394 . . . . 5
4 c2o 7143 . . . . 5
5 csdm 7535 . . . . 5
63, 4, 5wbr 4452 . . . 4
73, 3cxp 5002 . . . . 5
83, 7, 5wbr 4452 . . . 4
96, 8wo 368 . . 3
109, 2cab 2442 . 2
111, 10wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  isfin6  8701
  Copyright terms: Public domain W3C validator