Definition df-bj-ind 13544

Description: Define the property of being an inductive class. (Contributed by BJ, 30-Nov-2019.)

Assertion

Ref	Expression
df-bj-ind	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )

Distinct variable group:   x, A

Detailed syntax breakdown of Definition df-bj-ind

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wind 13543	. 2 wff Ind A
3		c0 3394	. . . 4 class (/)
4	3, 1	wcel 2128	. . 3 wff (/) e. A
5		vx	. . . . . . 7 setvar x
6	5	cv 1334	. . . . . 6 class x
7	6	csuc 4326	. . . . 5 class suc x
8	7, 1	wcel 2128	. . . 4 wff suc x e. A
9	8, 5, 1	wral 2435	. . 3 wff A. x e. A suc x e. A
10	4, 9	wa 103	. 2 wff ( (/) e. A /\ A. x e. A suc x e. A )
11	2, 10	wb 104	1 wff (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )

This definition is referenced by:  bj-indsuc  13545  bj-indeq  13546  bj-bdind  13547  bj-indint  13548  bj-indind  13549  bj-dfom  13550  bj-inf2vnlem1  13587  bj-inf2vnlem2  13588