ax-bd0 - Mathbox for BJ

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

Axiom ax-bd0 14501

Description: If two formulas are equivalent, then boundedness of one implies boundedness of the other. (Contributed by BJ, 3-Oct-2019.)

**Hypothesis**
Ref	Expression
ax-bd0.1

**Assertion**
Ref	Expression
ax-bd0	BOUNDED BOUNDED

**Detailed syntax breakdown of Axiom ax-bd0**
Step	Hyp	Ref	Expression
1		wph	. . 3
2	1	wbd 14500	. 2 BOUNDED
3		wps	. . 3
4	3	wbd 14500	. 2 BOUNDED
5	2, 4	wi 4	1 BOUNDED BOUNDED

Colors of variables: wff set class

This axiom is referenced by: bdeq 14511 bd0 14512