Theorem iunss 4982

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 4933	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 3954	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 3999	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		dfss2 3912	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3093	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3266	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3176	. . . 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 205  ∀wal 1537   ∈ wcel 2104  {cab 2713  ∀wral 3062  ∃wrex 3071   ⊆ wss 3892  ∪ ciun 4931

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rex 3072  df-v 3439  df-in 3899  df-ss 3909  df-iun 4933

This theorem is referenced by:  iunss2  4986  iunssd  4987  djussxp  5767  fiun  7817  f1iun  7818  frrlem7  8139  wfrdmssOLD  8177  onfununi  8203  oawordeulem  8416  oaabslem  8508  oaabs2  8510  omabslem  8511  omabs  8512  marypha2lem1  9238  ttrclselem1  9527  trcl  9530  r1val1  9588  rankuni2b  9655  rankval4  9669  rankbnd  9670  rankbnd2  9671  rankc1  9672  cfslb2n  10070  cfsmolem  10072  hsmexlem2  10229  axdc3lem2  10253  ac6  10282  wuncval2  10549  inar1  10577  tskuni  10585  grur1a  10621  fsuppmapnn0fiublem  13756  fsuppmapnn0fiub  13757  rtrclreclem4  14817  prmreclem4  16665  prmreclem5  16666  prdsval  17211  prdsbas  17213  imasaddfnlem  17284  imasvscafn  17293  imasvscaf  17295  isacs2  17407  mreacs  17412  acsfn  17413  dmcoass  17826  isacs5  18311  dprdspan  19675  dprd2dlem1  19689  dprd2d2  19692  dmdprdsplit2lem  19693  lbsextlem2  20466  lpival  20561  iunocv  20931  tgidm  22175  iunconn  22624  comppfsc  22728  txtube  22836  txcmplem2  22838  xkococnlem  22855  xkoinjcn  22883  alexsubALTlem3  23245  cnextf  23262  imasdsf1olem  23571  metnrmlem3  24069  ovolfiniun  24710  ovoliunlem2  24712  ovoliun  24714  ovoliunnul  24716  volfiniun  24756  voliunlem1  24759  volsup  24765  uniioombllem3a  24793  uniioombllem3  24794  uniioombllem4  24795  ismbf3d  24863  limciun  25103  taylfval  25563  taylf  25565  elpwiuncl  30921  disjunsn  30978  gsumpart  31360  esum2d  32106  omssubadd  32312  eulerpartlemgh  32390  eulerpartlemgs2  32392  bnj226  32758  bnj517  32910  bnj1118  33009  bnj1137  33020  cvmlift2lem12  33321  ntruni  34561  neibastop2lem  34594  filnetlem4  34615  mblfinlem2  35859  volsupnfl  35866  cnambfre  35869  sstotbnd2  35976  equivtotbnd  35980  totbndbnd  35991  prdstotbnd  35996  heiborlem1  36013  pclfinN  37956  lcfrlem4  39601  lcfrlem16  39614  lcfr  39641  iunrelexp0  41348  iunrelexpmin1  41354  iunrelexpmin2  41358  cotrcltrcl  41371  trclimalb2  41372  cotrclrcl  41388  iunconnlem2  42593  ixpssmapc  42660  ioorrnopnlem  43894  omeiunle  44105  omeiunltfirp  44107  carageniuncl  44111  caratheodorylem1  44114  caratheodorylem2  44115  hoissrrn  44137  ovnlecvr  44146  ovnsubaddlem1  44158  ovnsubadd  44160  hoissrrn2  44166  ovnlecvr2  44198  hspmbl  44217  opnvonmbllem2  44221  vonvolmbllem  44248  vonvolmbl2  44251  vonvol2  44252  iunhoiioolem  44263  iunhoiioo  44264