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

Theorem bdcuni 9996
 Description: The union of a setvar is a bounded class. (Contributed by BJ, 15-Oct-2019.)
Assertion
Ref Expression
bdcuni BOUNDED 𝑥

Proof of Theorem bdcuni
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-bdel 9941 . . . . 5 BOUNDED 𝑦𝑧
21ax-bdex 9939 . . . 4 BOUNDED𝑧𝑥 𝑦𝑧
32bdcab 9969 . . 3 BOUNDED {𝑦 ∣ ∃𝑧𝑥 𝑦𝑧}
4 df-rex 2312 . . . . 5 (∃𝑧𝑥 𝑦𝑧 ↔ ∃𝑧(𝑧𝑥𝑦𝑧))
5 exancom 1499 . . . . 5 (∃𝑧(𝑧𝑥𝑦𝑧) ↔ ∃𝑧(𝑦𝑧𝑧𝑥))
64, 5bitri 173 . . . 4 (∃𝑧𝑥 𝑦𝑧 ↔ ∃𝑧(𝑦𝑧𝑧𝑥))
76abbii 2153 . . 3 {𝑦 ∣ ∃𝑧𝑥 𝑦𝑧} = {𝑦 ∣ ∃𝑧(𝑦𝑧𝑧𝑥)}
83, 7bdceqi 9963 . 2 BOUNDED {𝑦 ∣ ∃𝑧(𝑦𝑧𝑧𝑥)}
9 df-uni 3581 . 2 𝑥 = {𝑦 ∣ ∃𝑧(𝑦𝑧𝑧𝑥)}
108, 9bdceqir 9964 1 BOUNDED 𝑥
 Colors of variables: wff set class Syntax hints:   ∧ wa 97  ∃wex 1381  {cab 2026  ∃wrex 2307  ∪ cuni 3580  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-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-bd0 9933  ax-bdex 9939  ax-bdel 9941  ax-bdsb 9942 This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-rex 2312  df-uni 3581  df-bdc 9961 This theorem is referenced by:  bj-uniex2  10036
 Copyright terms: Public domain W3C validator