Theorem sspwuni 5123

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		velpw 4627	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
2	1	ralbii 3099	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
3		dfss3 3997	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵)
4		unissb 4963	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
5	2, 3, 4	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 206   ∈ wcel 2108  ∀wral 3067   ⊆ wss 3976  𝒫 cpw 4622  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-v 3490  df-ss 3993  df-pw 4624  df-uni 4932

This theorem is referenced by:  pwssb  5124  elpwpw  5125  elpwuni  5128  intss2  5131  rintn0  5132  dftr4  5290  uniixp  8979  fipwss  9498  dffi3  9500  uniwf  9888  numacn  10118  dfac12lem2  10214  fin23lem32  10413  isf34lem4  10446  isf34lem5  10447  fin1a2lem12  10480  itunitc1  10489  fpwwe2lem11  10710  tsksuc  10831  unirnioo  13509  restid  17493  mrcuni  17679  isacs3lem  18612  dmdprdd  20043  dprdfeq0  20066  dprdres  20072  dprdss  20073  dprdz  20074  subgdmdprd  20078  subgdprd  20079  dprd2dlem1  20085  dprd2da  20086  dmdprdsplit2lem  20089  ablfac1b  20114  lssintcl  20985  lbsextlem2  21184  lbsextlem3  21185  cssmre  21734  topgele  22957  topontopn  22967  unitg  22995  fctop  23032  cctop  23034  ppttop  23035  epttop  23037  mretopd  23121  resttopon  23190  ordtuni  23219  conncompcld  23463  islocfin  23546  kgentopon  23567  txuni2  23594  ptuni2  23605  ptbasfi  23610  xkouni  23628  prdstopn  23657  txdis  23661  txcmplem2  23671  xkococnlem  23688  qtoptop2  23728  qtopuni  23731  tgqtop  23741  opnfbas  23871  neifil  23909  filunibas  23910  trfil1  23915  flimfil  23998  cldsubg  24140  tgpconncompeqg  24141  tgpconncomp  24142  tsmsxplem1  24182  utoptop  24264  unirnblps  24450  unirnbl  24451  setsmstopn  24511  tngtopn  24692  bndth  25009  bcthlem5  25381  ovolficcss  25523  ovollb  25533  voliunlem2  25605  voliunlem3  25606  uniioovol  25633  uniioombl  25643  opnmbllem  25655  ubthlem1  30902  hsupcl  31371  hsupss  31373  hsupunss  31375  hsupval2  31441  fnpreimac  32689  unicls  33849  pwsiga  34094  sigainb  34100  insiga  34101  pwldsys  34121  ddemeas  34200  omssubadd  34265  cvmsss2  35242  dfon2lem2  35748  ntruni  36293  clsint2  36295  neibastop1  36325  neibastop2lem  36326  neibastop3  36328  topmeet  36330  topjoin  36331  fnemeet1  36332  fnemeet2  36333  fnejoin1  36334  opnmbllem0  37616  heiborlem1  37771  elrfi  42650  pwpwuni  44959  0ome  46450