Theorem iunss 4979

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 4931	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 3953	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 3998	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		dfss2 3911	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3092	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3163	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3209	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8	7	albii 1825	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	5, 6, 8	3bitrri 297	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
10	2, 3, 9	3bitri 296	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539   ∈ wcel 2109  {cab 2716  ∀wral 3065  ∃wrex 3066   ⊆ wss 3891  ∪ ciun 4929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-nf 1790  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-v 3432  df-in 3898  df-ss 3908  df-iun 4931

This theorem is referenced by:  iunss2  4983  iunssd  4984  djussxp  5751  fiun  7772  f1iun  7773  frrlem7  8092  wfrdmssOLD  8130  onfununi  8156  oawordeulem  8361  oaabslem  8451  oaabs2  8453  omabslem  8454  omabs  8455  marypha2lem1  9155  ttrclselem1  9444  trpredlem1  9457  trpredss  9459  trpredmintr  9461  dftrpred3g  9464  trcl  9469  r1val1  9528  rankuni2b  9595  rankval4  9609  rankbnd  9610  rankbnd2  9611  rankc1  9612  cfslb2n  10008  cfsmolem  10010  hsmexlem2  10167  axdc3lem2  10191  ac6  10220  wuncval2  10487  inar1  10515  tskuni  10523  grur1a  10559  fsuppmapnn0fiublem  13691  fsuppmapnn0fiub  13692  rtrclreclem4  14753  prmreclem4  16601  prmreclem5  16602  prdsval  17147  prdsbas  17149  imasaddfnlem  17220  imasvscafn  17229  imasvscaf  17231  isacs2  17343  mreacs  17348  acsfn  17349  dmcoass  17762  isacs5  18247  dprdspan  19611  dprd2dlem1  19625  dprd2d2  19628  dmdprdsplit2lem  19629  lbsextlem2  20402  lpival  20497  iunocv  20867  tgidm  22111  iunconn  22560  comppfsc  22664  txtube  22772  txcmplem2  22774  xkococnlem  22791  xkoinjcn  22819  alexsubALTlem3  23181  cnextf  23198  imasdsf1olem  23507  metnrmlem3  24005  ovolfiniun  24646  ovoliunlem2  24648  ovoliun  24650  ovoliunnul  24652  volfiniun  24692  voliunlem1  24695  volsup  24701  uniioombllem3a  24729  uniioombllem3  24730  uniioombllem4  24731  ismbf3d  24799  limciun  25039  taylfval  25499  taylf  25501  elpwiuncl  30855  disjunsn  30912  gsumpart  31294  esum2d  32040  omssubadd  32246  eulerpartlemgh  32324  eulerpartlemgs2  32326  bnj226  32692  bnj517  32844  bnj1118  32943  bnj1137  32954  cvmlift2lem12  33255  ntruni  34495  neibastop2lem  34528  filnetlem4  34549  mblfinlem2  35794  volsupnfl  35801  cnambfre  35804  sstotbnd2  35911  equivtotbnd  35915  totbndbnd  35926  prdstotbnd  35931  heiborlem1  35948  pclfinN  37893  lcfrlem4  39538  lcfrlem16  39551  lcfr  39578  iunrelexp0  41263  iunrelexpmin1  41269  iunrelexpmin2  41273  cotrcltrcl  41286  trclimalb2  41287  cotrclrcl  41303  iunconnlem2  42508  ixpssmapc  42575  ioorrnopnlem  43799  omeiunle  44009  omeiunltfirp  44011  carageniuncl  44015  caratheodorylem1  44018  caratheodorylem2  44019  hoissrrn  44041  ovnlecvr  44050  ovnsubaddlem1  44062  ovnsubadd  44064  hoissrrn2  44070  ovnlecvr2  44102  hspmbl  44121  opnvonmbllem2  44125  vonvolmbllem  44152  vonvolmbl2  44155  vonvol2  44156  iunhoiioolem  44167  iunhoiioo  44168