Definition df-bj-ind 12088

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

Assertion

Ref	Expression
df-bj-ind	⊢ (Ind 𝐴 ↔ (∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))

Distinct variable group:   𝑥,𝐴

Detailed syntax breakdown of Definition df-bj-ind

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	wind 12087	. 2 wff Ind 𝐴
3		c0 3287	. . . 4 class ∅
4	3, 1	wcel 1439	. . 3 wff ∅ ∈ 𝐴
5		vx	. . . . . . 7 setvar 𝑥
6	5	cv 1289	. . . . . 6 class 𝑥
7	6	csuc 4201	. . . . 5 class suc 𝑥
8	7, 1	wcel 1439	. . . 4 wff suc 𝑥 ∈ 𝐴
9	8, 5, 1	wral 2360	. . 3 wff ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴
10	4, 9	wa 103	. 2 wff (∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴)
11	2, 10	wb 104	1 wff (Ind 𝐴 ↔ (∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))

This definition is referenced by:  bj-indsuc  12089  bj-indeq  12090  bj-bdind  12091  bj-indint  12092  bj-indind  12093  bj-dfom  12094  bj-inf2vnlem1  12131  bj-inf2vnlem2  12132