Theorem sspwuni 4643

Description: Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.)

Assertion

Ref	Expression
sspwuni	⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

Proof of Theorem sspwuni

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		selpw 4198	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
2	1	ralbii 3009	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
3		dfss3 3625	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵)
4		unissb 4501	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
5	2, 3, 4	3bitr4i 292	1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 196   ∈ wcel 2030  ∀wral 2941   ⊆ wss 3607  𝒫 cpw 4191  ∪ cuni 4468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-v 3233  df-in 3614  df-ss 3621  df-pw 4193  df-uni 4469

This theorem is referenced by:  pwssb  4644  elpwpw  4645  elpwuni  4648  rintn0  4651  dftr4  4790  uniixp  7973  fipwss  8376  dffi3  8378  uniwf  8720  numacn  8910  dfac12lem2  9004  fin23lem32  9204  isf34lem4  9237  isf34lem5  9238  fin1a2lem12  9271  itunitc1  9280  fpwwe2lem12  9501  tsksuc  9622  unirnioo  12311  restid  16141  mrcuni  16328  isacs3lem  17213  dmdprdd  18444  dprdfeq0  18467  dprdres  18473  dprdss  18474  dprdz  18475  subgdmdprd  18479  subgdprd  18480  dprd2dlem1  18486  dprd2da  18487  dmdprdsplit2lem  18490  ablfac1b  18515  lssintcl  19012  lbsextlem2  19207  lbsextlem3  19208  cssmre  20085  topgele  20782  topontopn  20792  unitg  20819  fctop  20856  cctop  20858  ppttop  20859  epttop  20861  mretopd  20944  toponmre  20945  resttopon  21013  ordtuni  21042  conncompcld  21285  islocfin  21368  kgentopon  21389  txuni2  21416  ptuni2  21427  ptbasfi  21432  xkouni  21450  prdstopn  21479  txdis  21483  txcmplem2  21493  xkococnlem  21510  qtoptop2  21550  qtopuni  21553  tgqtop  21563  opnfbas  21693  neifil  21731  filunibas  21732  trfil1  21737  flimfil  21820  cldsubg  21961  tgpconncompeqg  21962  tgpconncomp  21963  tsmsxplem1  22003  utoptop  22085  unirnblps  22271  unirnbl  22272  setsmstopn  22330  tngtopn  22501  bndth  22804  bcthlem5  23171  ovolficcss  23284  ovollb  23293  voliunlem2  23365  voliunlem3  23366  uniioovol  23393  uniioombl  23403  opnmbllem  23415  ubthlem1  27854  hsupcl  28326  hsupss  28328  hsupunss  28330  hsupval2  28396  unicls  30077  pwsiga  30321  sigainb  30327  insiga  30328  ddemeas  30427  omssubadd  30490  cvmsss2  31382  dfon2lem2  31813  ntruni  32447  clsint2  32449  neibastop1  32479  neibastop2lem  32480  neibastop3  32482  topmeet  32484  topjoin  32485  fnemeet1  32486  fnemeet2  32487  fnejoin1  32488  bj-intss  33178  opnmbllem0  33575  heiborlem1  33740  elrfi  37574  pwpwuni  39539  0ome  41064