Theorem iunss 5010

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 4961	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 3975	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 4022	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		dfss2 3933	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3092	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3267	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3175	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8	7	albii 1821	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	5, 6, 8	3bitrri 297	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
10	2, 3, 9	3bitri 296	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539   ∈ wcel 2106  {cab 2708  ∀wral 3060  ∃wrex 3069   ⊆ wss 3913  ∪ ciun 4959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-v 3448  df-in 3920  df-ss 3930  df-iun 4961

This theorem is referenced by:  iunss2  5014  iunssd  5015  djussxp  5806  fiun  7880  f1iun  7881  frrlem7  8228  wfrdmssOLD  8266  onfununi  8292  oawordeulem  8506  oaabslem  8598  oaabs2  8600  omabslem  8601  omabs  8602  marypha2lem1  9380  ttrclselem1  9670  trcl  9673  r1val1  9731  rankuni2b  9798  rankval4  9812  rankbnd  9813  rankbnd2  9814  rankc1  9815  cfslb2n  10213  cfsmolem  10215  hsmexlem2  10372  axdc3lem2  10396  ac6  10425  wuncval2  10692  inar1  10720  tskuni  10728  grur1a  10764  fsuppmapnn0fiublem  13905  fsuppmapnn0fiub  13906  rtrclreclem4  14958  prmreclem4  16802  prmreclem5  16803  prdsval  17351  prdsbas  17353  imasaddfnlem  17424  imasvscafn  17433  imasvscaf  17435  isacs2  17547  mreacs  17552  acsfn  17553  dmcoass  17966  isacs5  18451  dprdspan  19820  dprd2dlem1  19834  dprd2d2  19837  dmdprdsplit2lem  19838  lbsextlem2  20679  lpival  20774  iunocv  21122  tgidm  22367  iunconn  22816  comppfsc  22920  txtube  23028  txcmplem2  23030  xkococnlem  23047  xkoinjcn  23075  alexsubALTlem3  23437  cnextf  23454  imasdsf1olem  23763  metnrmlem3  24261  ovolfiniun  24902  ovoliunlem2  24904  ovoliun  24906  ovoliunnul  24908  volfiniun  24948  voliunlem1  24951  volsup  24957  uniioombllem3a  24985  uniioombllem3  24986  uniioombllem4  24987  ismbf3d  25055  limciun  25295  taylfval  25755  taylf  25757  elpwiuncl  31519  disjunsn  31579  gsumpart  31967  esum2d  32781  omssubadd  32989  eulerpartlemgh  33067  eulerpartlemgs2  33069  bnj226  33435  bnj517  33586  bnj1118  33685  bnj1137  33696  cvmlift2lem12  33995  ntruni  34875  neibastop2lem  34908  filnetlem4  34929  mblfinlem2  36189  volsupnfl  36196  cnambfre  36199  sstotbnd2  36306  equivtotbnd  36310  totbndbnd  36321  prdstotbnd  36326  heiborlem1  36343  pclfinN  38436  lcfrlem4  40081  lcfrlem16  40094  lcfr  40121  oaabsb  41687  naddgeoa  41788  naddwordnexlem4  41795  iunrelexp0  42096  iunrelexpmin1  42102  iunrelexpmin2  42106  cotrcltrcl  42119  trclimalb2  42120  cotrclrcl  42136  iunconnlem2  43339  ixpssmapc  43404  ioorrnopnlem  44665  omeiunle  44878  omeiunltfirp  44880  carageniuncl  44884  caratheodorylem1  44887  caratheodorylem2  44888  hoissrrn  44910  ovnlecvr  44919  ovnsubaddlem1  44931  ovnsubadd  44933  hoissrrn2  44939  ovnlecvr2  44971  hspmbl  44990  opnvonmbllem2  44994  vonvolmbllem  45021  vonvolmbl2  45024  vonvol2  45025  iunhoiioolem  45036  iunhoiioo  45037