![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > Mathboxes > ax-bd0 | GIF version |
Description: If two formulas are equivalent, then boundedness of one implies boundedness of the other. (Contributed by BJ, 3-Oct-2019.) |
Ref | Expression |
---|---|
ax-bd0.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
ax-bd0 | ⊢ (BOUNDED 𝜑 → BOUNDED 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | 1 | wbd 9932 | . 2 wff BOUNDED 𝜑 |
3 | wps | . . 3 wff 𝜓 | |
4 | 3 | wbd 9932 | . 2 wff BOUNDED 𝜓 |
5 | 2, 4 | wi 4 | 1 wff (BOUNDED 𝜑 → BOUNDED 𝜓) |
Colors of variables: wff set class |
This axiom is referenced by: bdeq 9943 bd0 9944 |
Copyright terms: Public domain | W3C validator |