Theorem sspwuni 4768

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 4322	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
2	1	ralbii 3127	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
3		dfss3 3750	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵)
4		unissb 4627	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
5	2, 3, 4	3bitr4i 294	1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 197   ∈ wcel 2155  ∀wral 3055   ⊆ wss 3732  𝒫 cpw 4315  ∪ cuni 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-v 3352  df-in 3739  df-ss 3746  df-pw 4317  df-uni 4595

This theorem is referenced by:  pwssb  4769  elpwpw  4770  elpwuni  4773  rintn0  4776  dftr4  4916  uniixp  8136  fipwss  8542  dffi3  8544  uniwf  8897  numacn  9123  dfac12lem2  9219  fin23lem32  9419  isf34lem4  9452  isf34lem5  9453  fin1a2lem12  9486  itunitc1  9495  fpwwe2lem12  9716  tsksuc  9837  unirnioo  12476  restid  16360  mrcuni  16547  isacs3lem  17432  dmdprdd  18665  dprdfeq0  18688  dprdres  18694  dprdss  18695  dprdz  18696  subgdmdprd  18700  subgdprd  18701  dprd2dlem1  18707  dprd2da  18708  dmdprdsplit2lem  18711  ablfac1b  18736  lssintcl  19236  lbsextlem2  19433  lbsextlem3  19434  cssmre  20313  topgele  21014  topontopn  21024  unitg  21051  fctop  21088  cctop  21090  ppttop  21091  epttop  21093  mretopd  21176  toponmre  21177  resttopon  21245  ordtuni  21274  conncompcld  21517  islocfin  21600  kgentopon  21621  txuni2  21648  ptuni2  21659  ptbasfi  21664  xkouni  21682  prdstopn  21711  txdis  21715  txcmplem2  21725  xkococnlem  21742  qtoptop2  21782  qtopuni  21785  tgqtop  21795  opnfbas  21925  neifil  21963  filunibas  21964  trfil1  21969  flimfil  22052  cldsubg  22193  tgpconncompeqg  22194  tgpconncomp  22195  tsmsxplem1  22235  utoptop  22317  unirnblps  22503  unirnbl  22504  setsmstopn  22562  tngtopn  22733  bndth  23036  bcthlem5  23405  ovolficcss  23527  ovollb  23537  voliunlem2  23609  voliunlem3  23610  uniioovol  23637  uniioombl  23647  opnmbllem  23659  ubthlem1  28182  hsupcl  28654  hsupss  28656  hsupunss  28658  hsupval2  28724  unicls  30396  pwsiga  30640  sigainb  30646  insiga  30647  ddemeas  30746  omssubadd  30809  cvmsss2  31704  dfon2lem2  32132  ntruni  32765  clsint2  32767  neibastop1  32797  neibastop2lem  32798  neibastop3  32800  topmeet  32802  topjoin  32803  fnemeet1  32804  fnemeet2  32805  fnejoin1  32806  bj-intss  33481  opnmbllem0  33869  heiborlem1  34032  elrfi  37935  pwpwuni  39876  0ome  41383