Definition df-bj-ind 9386

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

Assertion

Ref	Expression
df-bj-ind	⊢ (Ind A ↔ (∅ ∈ A ∧ ∀x ∈ A suc x ∈ 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 9385	. 2 wff Ind A
3		c0 3218	. . . 4 class ∅
4	3, 1	wcel 1390	. . 3 wff ∅ ∈ A
5		vx	. . . . . . 7 setvar x
6	5	cv 1241	. . . . . 6 class x
7	6	csuc 4068	. . . . 5 class suc x
8	7, 1	wcel 1390	. . . 4 wff suc x ∈ A
9	8, 5, 1	wral 2300	. . 3 wff ∀x ∈ A suc x ∈ A
10	4, 9	wa 97	. 2 wff (∅ ∈ A ∧ ∀x ∈ A suc x ∈ A)
11	2, 10	wb 98	1 wff (Ind A ↔ (∅ ∈ A ∧ ∀x ∈ A suc x ∈ A))

This definition is referenced by:  bj-indsuc  9387  bj-indeq  9388  bj-bdind  9389  bj-indint  9390  bj-indind  9391  bj-dfom  9392  peano5setOLD  9400  bj-inf2vnlem1  9430  bj-inf2vnlem2  9431