Theorem iunss 5012

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 4960	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 3978	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 4029	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		df-ss 3934	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3076	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3264	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3162	. . . 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 2109  {cab 2708  ∀wral 3045  ∃wrex 3054   ⊆ wss 3917  ∪ ciun 4958

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-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

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 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-ss 3934  df-iun 4960

This theorem is referenced by:  iunss2  5016  iunssd  5017  djussxp  5812  fiun  7924  f1iun  7925  frrlem7  8274  onfununi  8313  oawordeulem  8521  oaabslem  8614  oaabs2  8616  omabslem  8617  omabs  8618  marypha2lem1  9393  ttrclselem1  9685  trcl  9688  r1val1  9746  rankuni2b  9813  rankval4  9827  rankbnd  9828  rankbnd2  9829  rankc1  9830  cfslb2n  10228  cfsmolem  10230  hsmexlem2  10387  axdc3lem2  10411  ac6  10440  wuncval2  10707  inar1  10735  tskuni  10743  grur1a  10779  fsuppmapnn0fiublem  13962  fsuppmapnn0fiub  13963  rtrclreclem4  15034  prmreclem4  16897  prmreclem5  16898  prdsval  17425  prdsbas  17427  imasaddfnlem  17498  imasvscafn  17507  imasvscaf  17509  isacs2  17621  mreacs  17626  acsfn  17627  dmcoass  18035  isacs5  18514  dprdspan  19966  dprd2dlem1  19980  dprd2d2  19983  dmdprdsplit2lem  19984  lbsextlem2  21076  lpival  21241  iunocv  21597  tgidm  22874  iunconn  23322  comppfsc  23426  txtube  23534  txcmplem2  23536  xkococnlem  23553  xkoinjcn  23581  alexsubALTlem3  23943  cnextf  23960  imasdsf1olem  24268  metnrmlem3  24757  ovolfiniun  25409  ovoliunlem2  25411  ovoliun  25413  ovoliunnul  25415  volfiniun  25455  voliunlem1  25458  volsup  25464  uniioombllem3a  25492  uniioombllem3  25493  uniioombllem4  25494  ismbf3d  25562  limciun  25802  taylfval  26273  taylf  26275  elpwiuncl  32463  disjunsn  32530  gsumpart  33004  esum2d  34090  omssubadd  34298  eulerpartlemgh  34376  eulerpartlemgs2  34378  bnj226  34731  bnj517  34882  bnj1118  34981  bnj1137  34992  cvmlift2lem12  35308  ntruni  36322  neibastop2lem  36355  filnetlem4  36376  mblfinlem2  37659  volsupnfl  37666  cnambfre  37669  sstotbnd2  37775  equivtotbnd  37779  totbndbnd  37790  prdstotbnd  37795  heiborlem1  37812  pclfinN  39901  lcfrlem4  41546  lcfrlem16  41559  lcfr  41586  oaabsb  43290  naddgeoa  43390  naddwordnexlem4  43397  iunrelexp0  43698  iunrelexpmin1  43704  iunrelexpmin2  43708  cotrcltrcl  43721  trclimalb2  43722  cotrclrcl  43738  iunconnlem2  44931  ixpssmapc  45074  ioorrnopnlem  46309  omeiunle  46522  omeiunltfirp  46524  carageniuncl  46528  caratheodorylem1  46531  caratheodorylem2  46532  hoissrrn  46554  ovnlecvr  46563  ovnsubaddlem1  46575  ovnsubadd  46577  hoissrrn2  46583  ovnlecvr2  46615  hspmbl  46634  opnvonmbllem2  46638  vonvolmbllem  46665  vonvolmbl2  46668  vonvol2  46669  iunhoiioolem  46680  iunhoiioo  46681  iuneq0  48811  iuneqconst2  48815  imassc  49146