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  37708  volsupnfl  37715  cnambfre  37718  sstotbnd2  37824  equivtotbnd  37828  totbndbnd  37839  prdstotbnd  37844  heiborlem1  37861  pclfinN  40009  lcfrlem4  41654  lcfrlem16  41667  lcfr  41694  oaabsb  43397  naddgeoa  43497  naddwordnexlem4  43504  iunrelexp0  43805  iunrelexpmin1  43811  iunrelexpmin2  43815  cotrcltrcl  43828  trclimalb2  43829  cotrclrcl  43845  iunconnlem2  45037  ixpssmapc  45180  ioorrnopnlem  46412  omeiunle  46625  omeiunltfirp  46627  carageniuncl  46631  caratheodorylem1  46634  caratheodorylem2  46635  hoissrrn  46657  ovnlecvr  46666  ovnsubaddlem1  46678  ovnsubadd  46680  hoissrrn2  46686  ovnlecvr2  46718  hspmbl  46737  opnvonmbllem2  46741  vonvolmbllem  46768  vonvolmbl2  46771  vonvol2  46772  iunhoiioolem  46783  iunhoiioo  46784  iuneq0  48929  iuneqconst2  48933  imassc  49264