Theorem sspwuni 5052

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 4558	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
2	1	ralbii 3075	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
3		dfss3 3926	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵)
4		unissb 4893	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
5	2, 3, 4	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 206   ∈ wcel 2109  ∀wral 3044   ⊆ wss 3905  𝒫 cpw 4553  ∪ cuni 4861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3440  df-ss 3922  df-pw 4555  df-uni 4862

This theorem is referenced by:  pwssb  5053  elpwpw  5054  elpwuni  5057  intss2  5060  rintn0  5061  dftr4  5208  uniixp  8855  fipwss  9338  dffi3  9340  uniwf  9734  numacn  9962  dfac12lem2  10058  fin23lem32  10257  isf34lem4  10290  isf34lem5  10291  fin1a2lem12  10324  itunitc1  10333  fpwwe2lem11  10554  tsksuc  10675  unirnioo  13370  restid  17355  mrcuni  17545  isacs3lem  18466  dmdprdd  19898  dprdfeq0  19921  dprdres  19927  dprdss  19928  dprdz  19929  subgdmdprd  19933  subgdprd  19934  dprd2dlem1  19940  dprd2da  19941  dmdprdsplit2lem  19944  ablfac1b  19969  lssintcl  20885  lbsextlem2  21084  lbsextlem3  21085  cssmre  21618  topgele  22833  topontopn  22843  unitg  22870  fctop  22907  cctop  22909  ppttop  22910  epttop  22912  mretopd  22995  resttopon  23064  ordtuni  23093  conncompcld  23337  islocfin  23420  kgentopon  23441  txuni2  23468  ptuni2  23479  ptbasfi  23484  xkouni  23502  prdstopn  23531  txdis  23535  txcmplem2  23545  xkococnlem  23562  qtoptop2  23602  qtopuni  23605  tgqtop  23615  opnfbas  23745  neifil  23783  filunibas  23784  trfil1  23789  flimfil  23872  cldsubg  24014  tgpconncompeqg  24015  tgpconncomp  24016  tsmsxplem1  24056  utoptop  24138  unirnblps  24323  unirnbl  24324  setsmstopn  24382  tngtopn  24554  bndth  24873  bcthlem5  25244  ovolficcss  25386  ovollb  25396  voliunlem2  25468  voliunlem3  25469  uniioovol  25496  uniioombl  25506  opnmbllem  25518  ubthlem1  30832  hsupcl  31301  hsupss  31303  hsupunss  31305  hsupval2  31371  fnpreimac  32628  unicls  33869  pwsiga  34096  sigainb  34102  insiga  34103  pwldsys  34123  ddemeas  34202  omssubadd  34267  cvmsss2  35246  dfon2lem2  35757  ntruni  36300  clsint2  36302  neibastop1  36332  neibastop2lem  36333  neibastop3  36335  topmeet  36337  topjoin  36338  fnemeet1  36339  fnemeet2  36340  fnejoin1  36341  opnmbllem0  37635  heiborlem1  37790  elrfi  42667  pwpwuni  45035  0ome  46511