Theorem iunss 4992

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 4941	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 3958	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 4009	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		df-ss 3914	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3078	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3258	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3159	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8	7	albii 1820	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	5, 6, 8	3bitrri 298	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
10	2, 3, 9	3bitri 297	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   ∈ wcel 2111  {cab 2709  ∀wral 3047  ∃wrex 3056   ⊆ wss 3897  ∪ ciun 4939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-ss 3914  df-iun 4941

This theorem is referenced by:  iunss2  4996  iunssd  4997  djussxp  5784  fiun  7875  f1iun  7876  frrlem7  8222  onfununi  8261  oawordeulem  8469  oaabslem  8562  oaabs2  8564  omabslem  8565  omabs  8566  marypha2lem1  9319  ttrclselem1  9615  trcl  9618  r1val1  9679  rankuni2b  9746  rankval4  9760  rankbnd  9761  rankbnd2  9762  rankc1  9763  cfslb2n  10159  cfsmolem  10161  hsmexlem2  10318  axdc3lem2  10342  ac6  10371  wuncval2  10638  inar1  10666  tskuni  10674  grur1a  10710  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  rtrclreclem4  14968  prmreclem4  16831  prmreclem5  16832  prdsval  17359  prdsbas  17361  imasaddfnlem  17432  imasvscafn  17441  imasvscaf  17443  isacs2  17559  mreacs  17564  acsfn  17565  dmcoass  17973  isacs5  18454  dprdspan  19941  dprd2dlem1  19955  dprd2d2  19958  dmdprdsplit2lem  19959  lbsextlem2  21096  lpival  21261  iunocv  21618  tgidm  22895  iunconn  23343  comppfsc  23447  txtube  23555  txcmplem2  23557  xkococnlem  23574  xkoinjcn  23602  alexsubALTlem3  23964  cnextf  23981  imasdsf1olem  24288  metnrmlem3  24777  ovolfiniun  25429  ovoliunlem2  25431  ovoliun  25433  ovoliunnul  25435  volfiniun  25475  voliunlem1  25478  volsup  25484  uniioombllem3a  25512  uniioombllem3  25513  uniioombllem4  25514  ismbf3d  25582  limciun  25822  taylfval  26293  taylf  26295  bdayle  27861  elpwiuncl  32507  disjunsn  32574  gsumpart  33037  esum2d  34106  omssubadd  34313  eulerpartlemgh  34391  eulerpartlemgs2  34393  bnj226  34746  bnj517  34897  bnj1118  34996  bnj1137  35007  rankval4b  35111  tz9.1regs  35130  cvmlift2lem12  35358  ntruni  36371  neibastop2lem  36404  filnetlem4  36425  mblfinlem2  37697  volsupnfl  37704  cnambfre  37707  sstotbnd2  37813  equivtotbnd  37817  totbndbnd  37828  prdstotbnd  37833  heiborlem1  37850  pclfinN  39998  lcfrlem4  41643  lcfrlem16  41656  lcfr  41683  oaabsb  43386  naddgeoa  43486  naddwordnexlem4  43493  iunrelexp0  43794  iunrelexpmin1  43800  iunrelexpmin2  43804  cotrcltrcl  43817  trclimalb2  43818  cotrclrcl  43834  iunconnlem2  45026  ixpssmapc  45169  ioorrnopnlem  46401  omeiunle  46614  omeiunltfirp  46616  carageniuncl  46620  caratheodorylem1  46623  caratheodorylem2  46624  hoissrrn  46646  ovnlecvr  46655  ovnsubaddlem1  46667  ovnsubadd  46669  hoissrrn2  46675  ovnlecvr2  46707  hspmbl  46726  opnvonmbllem2  46730  vonvolmbllem  46757  vonvolmbl2  46760  vonvol2  46761  iunhoiioolem  46772  iunhoiioo  46773  iuneq0  48918  iuneqconst2  48922  imassc  49253