ax-bj-d0cl - Mathbox for BJ

	Mathbox for BJ		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > Mathboxes > ax-bj-d0cl		Unicode version

Axiom ax-bj-d0cl 15580

Description: Axiom for Δ₀-classical logic. (Contributed by BJ, 2-Jan-2020.)

**Hypothesis**
Ref	Expression
ax-bj-d0class.bd	BOUNDED

**Assertion**
Ref	Expression
ax-bj-d0cl	DECID

**Detailed syntax breakdown of Axiom ax-bj-d0cl**
Step	Hyp	Ref	Expression
1		wph	. 2
2	1	wdc 835	1 DECID

Colors of variables: wff set class

This axiom is referenced by: bj-d0clsepcl 15581