Definition df-fin5

Description: A set is V-finite iff it behaves finitely under |_| . Definition V of Levy58 p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014)

	Ref	Expression
Assertion	df-fin5	$$⊢{\mathrm{Fin}}^{\mathrm{V}}=\left\{x|\left(x=\varnothing \vee x\prec \left(x\mathrm{\bigsqcup ︀}x\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin5	$$class{\mathrm{Fin}}^{\mathrm{V}}$$
1		vx	$$setvarx$$
2	1	cv	$$setvarx$$
3		c0	$$class\varnothing$$
4	2 3	wceq	$$wffx=\varnothing$$
5		csdm	$$class\prec$$
6	2 2	cdju	$$class\left(x\mathrm{\bigsqcup ︀}x\right)$$
7	2 6 5	wbr	$$wffx\prec \left(x\mathrm{\bigsqcup ︀}x\right)$$
8	4 7	wo	$$wff\left(x=\varnothing \vee x\prec \left(x\mathrm{\bigsqcup ︀}x\right)\right)$$
9	8 1	cab	$$class\left\{x|\left(x=\varnothing \vee x\prec \left(x\mathrm{\bigsqcup ︀}x\right)\right)\right\}$$
10	0 9	wceq	$$wff{\mathrm{Fin}}^{\mathrm{V}}=\left\{x|\left(x=\varnothing \vee x\prec \left(x\mathrm{\bigsqcup ︀}x\right)\right)\right\}$$