Definition df-bdc 17038

Description: Define a bounded class as one such that membership in this class is a bounded formula. (Contributed by BJ, 3-Oct-2019.)

Assertion

Ref	Expression
df-bdc	⊢ (BOUNDED 𝐴 ↔ ∀𝑥BOUNDED 𝑥 ∈ 𝐴)

Distinct variable group:   𝑥,𝐴

Detailed syntax breakdown of Definition df-bdc

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	wbdc 17037	. 2 wff BOUNDED 𝐴
3		vx	. . . . . 6 setvar 𝑥
4	3	cv 1401	. . . . 5 class 𝑥
5	4, 1	wcel 2209	. . . 4 wff 𝑥 ∈ 𝐴
6	5	wbd 17009	. . 3 wff BOUNDED 𝑥 ∈ 𝐴
7	6, 3	wal 1400	. 2 wff ∀𝑥BOUNDED 𝑥 ∈ 𝐴
8	2, 7	wb 105	1 wff (BOUNDED 𝐴 ↔ ∀𝑥BOUNDED 𝑥 ∈ 𝐴)

This definition is used by:  bdceq  17039  bdel  17042  bdelir  17044