Theorem sspwuni 5067

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

Syntax hints:   ↔ wb 209   ∈ wcel 2143  ∀wral 3079   ⊆ wss 3906  𝒫 cpw 4563  ∪ cuni 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-v 3457  df-ss 3923  df-pw 4565  df-uni 4874

This theorem is referenced by:  pwssb  5068  elpwpw  5069  elpwuni  5072  intss2  5075  rintn0  5076  dftr4  5225  uniixp  8920  fipwss  9390  dffi3  9392  uniwf  9792  numacn  10034  dfac12lem2  10129  fin23lem32  10329  isf34lem4  10362  isf34lem5  10363  fin1a2lem12  10396  itunitc1  10405  fpwwe2lem11  10627  tsksuc  10748  unirnioo  13477  restid  17487  mrcuni  17678  isacs3lem  18599  dmdprdd  20072  dprdfeq0  20095  dprdres  20101  dprdss  20102  dprdz  20103  subgdmdprd  20107  subgdprd  20108  dprd2dlem1  20114  dprd2da  20115  dmdprdsplit2lem  20118  ablfac1b  20143  lssintcl  21066  lbsextlem2  21264  lbsextlem3  21265  cssmre  21824  topgele  23068  topontopn  23078  unitg  23105  fctop  23142  cctop  23144  ppttop  23145  epttop  23147  mretopd  23230  resttopon  23299  ordtuni  23328  conncompcld  23572  islocfin  23655  kgentopon  23676  txuni2  23703  ptuni2  23714  ptbasfi  23719  xkouni  23737  prdstopn  23766  txdis  23770  txcmplem2  23780  xkococnlem  23797  qtoptop2  23837  qtopuni  23840  tgqtop  23850  opnfbas  23980  neifil  24018  filunibas  24019  trfil1  24024  flimfil  24107  cldsubg  24249  tgpconncompeqg  24250  tgpconncomp  24251  tsmsxplem1  24291  utoptop  24372  unirnblps  24557  unirnbl  24558  setsmstopn  24616  tngtopn  24788  bndth  25098  bcthlem5  25468  ovolficcss  25609  ovollb  25619  voliunlem2  25691  voliunlem3  25692  uniioovol  25719  uniioombl  25729  opnmbllem  25741  ubthlem1  31203  hsupcl  31672  hsupss  31674  hsupunss  31676  hsupval2  31742  fnpreimac  32996  unicls  34274  pwsiga  34501  sigainb  34507  insiga  34508  pwldsys  34528  ddemeas  34607  omssubadd  34671  cvmsss2  35747  dfon2lem2  36255  ntruni  36819  clsint2  36821  neibastop1  36851  neibastop2lem  36852  neibastop3  36854  topmeet  36856  topjoin  36857  fnemeet1  36858  fnemeet2  36859  fnejoin1  36860  opnmbllem0  38288  heiborlem1  38443  elrfi  43408  pwpwuni  45760  0ome  47226