Theorem bdcuni 9265

Description: The union of a setvar is a bounded class. (Contributed by BJ, 15-Oct-2019.)

Assertion

Ref	Expression
bdcuni	⊢ BOUNDED ∪ x

Proof of Theorem bdcuni

Dummy variables y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-bdel 9210	. . . . 5 ⊢ BOUNDED y ∈ z
2	1	ax-bdex 9208	. . . 4 ⊢ BOUNDED ∃z ∈ x y ∈ z
3	2	bdcab 9238	. . 3 ⊢ BOUNDED {y ∣ ∃z ∈ x y ∈ z}
4		df-rex 2306	. . . . 5 ⊢ (∃z ∈ x y ∈ z ↔ ∃z(z ∈ x ∧ y ∈ z))
5		exancom 1496	. . . . 5 ⊢ (∃z(z ∈ x ∧ y ∈ z) ↔ ∃z(y ∈ z ∧ z ∈ x))
6	4, 5	bitri 173	. . . 4 ⊢ (∃z ∈ x y ∈ z ↔ ∃z(y ∈ z ∧ z ∈ x))
7	6	abbii 2150	. . 3 ⊢ {y ∣ ∃z ∈ x y ∈ z} = {y ∣ ∃z(y ∈ z ∧ z ∈ x)}
8	3, 7	bdceqi 9232	. 2 ⊢ BOUNDED {y ∣ ∃z(y ∈ z ∧ z ∈ x)}
9		df-uni 3572	. 2 ⊢ ∪ x = {y ∣ ∃z(y ∈ z ∧ z ∈ x)}
10	8, 9	bdceqir 9233	1 ⊢ BOUNDED ∪ x

Syntax hints:   ∧ wa 97  ∃wex 1378  {cab 2023  ∃wrex 2301  ∪ cuni 3571  BOUNDED wbdc 9229

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 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-bd0 9202  ax-bdex 9208  ax-bdel 9210  ax-bdsb 9211

This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-rex 2306  df-uni 3572  df-bdc 9230

This theorem is referenced by:  bj-uniex2  9301