Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bdceq GIF version

Theorem bdceq 9962
 Description: Equality property for the predicate BOUNDED. (Contributed by BJ, 3-Oct-2019.)
Hypothesis
Ref Expression
bdceq.1 𝐴 = 𝐵
Assertion
Ref Expression
bdceq (BOUNDED 𝐴BOUNDED 𝐵)

Proof of Theorem bdceq
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 bdceq.1 . . . . 5 𝐴 = 𝐵
21eleq2i 2104 . . . 4 (𝑥𝐴𝑥𝐵)
32bdeq 9943 . . 3 (BOUNDED 𝑥𝐴BOUNDED 𝑥𝐵)
43albii 1359 . 2 (∀𝑥BOUNDED 𝑥𝐴 ↔ ∀𝑥BOUNDED 𝑥𝐵)
5 df-bdc 9961 . 2 (BOUNDED 𝐴 ↔ ∀𝑥BOUNDED 𝑥𝐴)
6 df-bdc 9961 . 2 (BOUNDED 𝐵 ↔ ∀𝑥BOUNDED 𝑥𝐵)
74, 5, 63bitr4i 201 1 (BOUNDED 𝐴BOUNDED 𝐵)
 Colors of variables: wff set class Syntax hints:   ↔ wb 98  ∀wal 1241   = wceq 1243   ∈ wcel 1393  BOUNDED wbd 9932  BOUNDED wbdc 9960 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022  ax-bd0 9933 This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036  df-bdc 9961 This theorem is referenced by:  bdceqi  9963
 Copyright terms: Public domain W3C validator