Theorem sspwuni 4547

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 4115	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
2	1	ralbii 2963	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
3		dfss3 3558	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵)
4		unissb 4405	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
5	2, 3, 4	3bitr4i 291	1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 195   ∈ wcel 1977  ∀wral 2896   ⊆ wss 3540  𝒫 cpw 4108  ∪ cuni 4372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110  df-uni 4373

This theorem is referenced by:  pwssb  4548  elpwuni  4549  rintn0  4552  dftr4  4685  uniixp  7817  fipwss  8218  dffi3  8220  uniwf  8565  numacn  8755  dfac12lem2  8849  fin23lem32  9049  isf34lem4  9082  isf34lem5  9083  fin1a2lem12  9116  itunitc1  9125  fpwwe2lem12  9342  tsksuc  9463  unirnioo  12144  restid  15917  mrcuni  16104  isacs3lem  16989  dmdprdd  18221  dprdfeq0  18244  dprdres  18250  dprdss  18251  dprdz  18252  subgdmdprd  18256  subgdprd  18257  dprd2dlem1  18263  dprd2da  18264  dmdprdsplit2lem  18267  ablfac1b  18292  lssintcl  18785  lbsextlem2  18980  lbsextlem3  18981  cssmre  19856  topgele  20549  topontopn  20557  unitg  20582  fctop  20618  cctop  20620  ppttop  20621  epttop  20623  mretopd  20706  toponmre  20707  resttopon  20775  ordtuni  20804  concompcld  21047  islocfin  21130  kgentopon  21151  txuni2  21178  ptuni2  21189  ptbasfi  21194  xkouni  21212  prdstopn  21241  txdis  21245  txcmplem2  21255  xkococnlem  21272  qtoptop2  21312  qtopuni  21315  tgqtop  21325  opnfbas  21456  neifil  21494  filunibas  21495  trfil1  21500  flimfil  21583  cldsubg  21724  tgpconcompeqg  21725  tgpconcomp  21726  tsmsxplem1  21766  utoptop  21848  unirnblps  22034  unirnbl  22035  setsmstopn  22093  tngtopn  22264  bndth  22565  bcthlem5  22933  ovolficcss  23045  ovollb  23054  voliunlem2  23126  voliunlem3  23127  uniioovol  23153  uniioombl  23163  opnmbllem  23175  ubthlem1  27110  hsupcl  27582  hsupss  27584  hsupunss  27586  hsupval2  27652  unicls  29277  pwsiga  29520  sigainb  29526  insiga  29527  ddemeas  29626  omssubadd  29689  cvmsss2  30510  dfon2lem2  30933  ntruni  31492  clsint2  31494  neibastop1  31524  neibastop2lem  31525  neibastop3  31527  topmeet  31529  topjoin  31530  fnemeet1  31531  fnemeet2  31532  fnejoin1  31533  bj-sspwpw  32238  opnmbllem0  32615  heiborlem1  32780  elrfi  36275  pwpwuni  38250  0ome  39419