Definition df-bdc 7068

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 A ↔ ∀xBOUNDED x ∈ A)

Distinct variable group:   x,A

Detailed syntax breakdown of Definition df-bdc

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wbdc 7067	. 2 wff BOUNDED A
3		vx	. . . . . 6 setvar x
4	3	cv 1227	. . . . 5 class x
5	4, 1	wcel 1374	. . . 4 wff x ∈ A
6	5	wbd 7039	. . 3 wff BOUNDED x ∈ A
7	6, 3	wal 1226	. 2 wff ∀xBOUNDED x ∈ A
8	2, 7	wb 98	1 wff (BOUNDED A ↔ ∀xBOUNDED x ∈ A)

This definition is referenced by:  bdceq  7069  bdel  7072  bdelir  7074