Metamath Proof Explorer


Definition df-fin6

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)

Ref Expression
Assertion df-fin6 FinVI = x | x 2 𝑜 x x × x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfin6 class FinVI
1 vx setvar x
2 1 cv setvar x
3 csdm class
4 c2o class 2 𝑜
5 2 4 3 wbr wff x 2 𝑜
6 2 2 cxp class x × x
7 2 6 3 wbr wff x x × x
8 5 7 wo wff x 2 𝑜 x x × x
9 8 1 cab class x | x 2 𝑜 x x × x
10 0 9 wceq wff FinVI = x | x 2 𝑜 x x × x