Theorem iunss 5021

Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

Ref	Expression
iunss	⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Distinct variable group:   𝑥,𝐶

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem iunss

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iun 4969	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 3987	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 4038	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		df-ss 3943	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3082	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3268	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3168	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8	7	albii 1819	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	5, 6, 8	3bitrri 298	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
10	2, 3, 9	3bitri 297	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   ∈ wcel 2108  {cab 2713  ∀wral 3051  ∃wrex 3060   ⊆ wss 3926  ∪ ciun 4967

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-ss 3943  df-iun 4969

This theorem is referenced by:  iunss2  5025  iunssd  5026  djussxp  5825  fiun  7941  f1iun  7942  frrlem7  8291  wfrdmssOLD  8329  onfununi  8355  oawordeulem  8566  oaabslem  8659  oaabs2  8661  omabslem  8662  omabs  8663  marypha2lem1  9447  ttrclselem1  9739  trcl  9742  r1val1  9800  rankuni2b  9867  rankval4  9881  rankbnd  9882  rankbnd2  9883  rankc1  9884  cfslb2n  10282  cfsmolem  10284  hsmexlem2  10441  axdc3lem2  10465  ac6  10494  wuncval2  10761  inar1  10789  tskuni  10797  grur1a  10833  fsuppmapnn0fiublem  14008  fsuppmapnn0fiub  14009  rtrclreclem4  15080  prmreclem4  16939  prmreclem5  16940  prdsval  17469  prdsbas  17471  imasaddfnlem  17542  imasvscafn  17551  imasvscaf  17553  isacs2  17665  mreacs  17670  acsfn  17671  dmcoass  18079  isacs5  18558  dprdspan  20010  dprd2dlem1  20024  dprd2d2  20027  dmdprdsplit2lem  20028  lbsextlem2  21120  lpival  21285  iunocv  21641  tgidm  22918  iunconn  23366  comppfsc  23470  txtube  23578  txcmplem2  23580  xkococnlem  23597  xkoinjcn  23625  alexsubALTlem3  23987  cnextf  24004  imasdsf1olem  24312  metnrmlem3  24801  ovolfiniun  25454  ovoliunlem2  25456  ovoliun  25458  ovoliunnul  25460  volfiniun  25500  voliunlem1  25503  volsup  25509  uniioombllem3a  25537  uniioombllem3  25538  uniioombllem4  25539  ismbf3d  25607  limciun  25847  taylfval  26318  taylf  26320  elpwiuncl  32508  disjunsn  32575  gsumpart  33051  esum2d  34124  omssubadd  34332  eulerpartlemgh  34410  eulerpartlemgs2  34412  bnj226  34765  bnj517  34916  bnj1118  35015  bnj1137  35026  cvmlift2lem12  35336  ntruni  36345  neibastop2lem  36378  filnetlem4  36399  mblfinlem2  37682  volsupnfl  37689  cnambfre  37692  sstotbnd2  37798  equivtotbnd  37802  totbndbnd  37813  prdstotbnd  37818  heiborlem1  37835  pclfinN  39919  lcfrlem4  41564  lcfrlem16  41577  lcfr  41604  oaabsb  43318  naddgeoa  43418  naddwordnexlem4  43425  iunrelexp0  43726  iunrelexpmin1  43732  iunrelexpmin2  43736  cotrcltrcl  43749  trclimalb2  43750  cotrclrcl  43766  iunconnlem2  44959  ixpssmapc  45097  ioorrnopnlem  46333  omeiunle  46546  omeiunltfirp  46548  carageniuncl  46552  caratheodorylem1  46555  caratheodorylem2  46556  hoissrrn  46578  ovnlecvr  46587  ovnsubaddlem1  46599  ovnsubadd  46601  hoissrrn2  46607  ovnlecvr2  46639  hspmbl  46658  opnvonmbllem2  46662  vonvolmbllem  46689  vonvolmbl2  46692  vonvol2  46693  iunhoiioolem  46704  iunhoiioo  46705  iuneq0  48797  iuneqconst2  48801  imassc  49093