Theorem sspwuni 5059

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 4561	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
2	1	ralbii 3108	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
3		dfss3 3897	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵)
4		unissb 4900	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
5	2, 3, 4	3bitr4i 306	1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2144  ∀wral 3076   ⊆ wss 3895  𝒫 cpw 4556  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3896  df-pw 4558  df-uni 4867

This theorem is used by:  pwssb  5060  elpwpw  5061  elpwuni  5064  intss2  5067  rintn0  5068  dftr4  5217  uniixp  8952  fipwss  9424  dffi3  9426  uniwf  9831  numacn  10131  dfac12lem2  10226  fin23lem32  10425  isf34lem4  10458  isf34lem5  10459  fin1a2lem12  10492  itunitc1  10501  fpwwe2lem11  10729  tsksuc  10850  unirnioo  13583  restid  17609  mrcuni  17800  isacs3lem  18721  dmdprdd  20220  dprdfeq0  20243  dprdres  20249  dprdss  20250  dprdz  20251  subgdmdprd  20255  subgdprd  20256  dprd2dlem1  20262  dprd2da  20263  dmdprdsplit2lem  20266  ablfac1b  20291  lssintcl  21244  lbsextlem2  21442  lbsextlem3  21443  cssmre  22004  topgele  23253  topontopn  23263  unitg  23290  fctop  23327  cctop  23329  ppttop  23330  epttop  23332  mretopd  23415  resttopon  23484  ordtuni  23513  conncompcld  23757  islocfin  23841  kgentopon  23862  txuni2  23889  ptuni2  23900  ptbasfi  23905  xkouni  23923  prdstopn  23952  txdis  23956  txcmplem2  23966  xkococnlem  23983  qtoptop2  24023  qtopuni  24026  tgqtop  24036  opnfbas  24166  neifil  24204  filunibas  24205  trfil1  24210  flimfil  24293  cldsubg  24435  tgpconncompeqg  24436  tgpconncomp  24437  tsmsxplem1  24477  utoptop  24558  unirnblps  24743  unirnbl  24744  setsmstopn  24802  tngtopn  24974  bndth  25284  bcthlem5  25654  ovolficcss  25795  ovollb  25805  voliunlem2  25877  voliunlem3  25878  uniioovol  25905  uniioombl  25915  opnmbllem  25927  ubthlem1  31477  hsupcl  31946  hsupss  31948  hsupunss  31950  hsupval2  32016  fnpreimac  33311  reff  34517  unicls  34581  pwsiga  34808  sigainb  34815  insiga  34816  pwldsys  34836  ddemeas  34915  omssubadd  34978  cvmsss2  36125  dfon2lem2  36638  ntruni  37207  clsint2  37209  neibastop1  37239  neibastop2lem  37240  neibastop3  37242  topmeet  37244  topjoin  37245  fnemeet1  37246  fnemeet2  37247  fnejoin1  37248  opnmbllem0  38667  heiborlem1  38838  elrfi  43798  pwpwuni  46167  0ome  47632