Theorem sspwuni 5047

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 4552	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
2	1	ralbii 3092	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
3		dfss3 3920	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵)
4		unissb 4887	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
5	2, 3, 4	3bitr4i 302	1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 205   ∈ wcel 2105  ∀wral 3061   ⊆ wss 3898  𝒫 cpw 4547  ∪ cuni 4852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-v 3443  df-in 3905  df-ss 3915  df-pw 4549  df-uni 4853

This theorem is referenced by:  pwssb  5048  elpwpw  5049  elpwuni  5052  intss2  5055  rintn0  5056  dftr4  5216  uniixp  8780  fipwss  9286  dffi3  9288  uniwf  9676  numacn  9906  dfac12lem2  10001  fin23lem32  10201  isf34lem4  10234  isf34lem5  10235  fin1a2lem12  10268  itunitc1  10277  fpwwe2lem11  10498  tsksuc  10619  unirnioo  13282  restid  17241  mrcuni  17427  isacs3lem  18357  dmdprdd  19697  dprdfeq0  19720  dprdres  19726  dprdss  19727  dprdz  19728  subgdmdprd  19732  subgdprd  19733  dprd2dlem1  19739  dprd2da  19740  dmdprdsplit2lem  19743  ablfac1b  19768  lssintcl  20332  lbsextlem2  20527  lbsextlem3  20528  cssmre  21004  topgele  22185  topontopn  22195  unitg  22223  fctop  22260  cctop  22262  ppttop  22263  epttop  22265  mretopd  22349  resttopon  22418  ordtuni  22447  conncompcld  22691  islocfin  22774  kgentopon  22795  txuni2  22822  ptuni2  22833  ptbasfi  22838  xkouni  22856  prdstopn  22885  txdis  22889  txcmplem2  22899  xkococnlem  22916  qtoptop2  22956  qtopuni  22959  tgqtop  22969  opnfbas  23099  neifil  23137  filunibas  23138  trfil1  23143  flimfil  23226  cldsubg  23368  tgpconncompeqg  23369  tgpconncomp  23370  tsmsxplem1  23410  utoptop  23492  unirnblps  23678  unirnbl  23679  setsmstopn  23739  tngtopn  23920  bndth  24227  bcthlem5  24598  ovolficcss  24739  ovollb  24749  voliunlem2  24821  voliunlem3  24822  uniioovol  24849  uniioombl  24859  opnmbllem  24871  ubthlem1  29520  hsupcl  29989  hsupss  29991  hsupunss  29993  hsupval2  30059  fnpreimac  31295  unicls  32151  pwsiga  32396  sigainb  32402  insiga  32403  pwldsys  32423  ddemeas  32502  omssubadd  32567  cvmsss2  33535  dfon2lem2  34043  ntruni  34612  clsint2  34614  neibastop1  34644  neibastop2lem  34645  neibastop3  34647  topmeet  34649  topjoin  34650  fnemeet1  34651  fnemeet2  34652  fnejoin1  34653  opnmbllem0  35926  heiborlem1  36082  elrfi  40786  pwpwuni  42934  0ome  44413