Theorem iunss 5050

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 4998	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 4024	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 4073	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		df-ss 3980	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3091	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3284	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3181	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8	7	albii 1816	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	5, 6, 8	3bitrri 298	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
10	2, 3, 9	3bitri 297	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535   ∈ wcel 2106  {cab 2712  ∀wral 3059  ∃wrex 3068   ⊆ wss 3963  ∪ ciun 4996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-ss 3980  df-iun 4998

This theorem is referenced by:  iunss2  5054  iunssd  5055  djussxp  5859  fiun  7966  f1iun  7967  frrlem7  8316  wfrdmssOLD  8354  onfununi  8380  oawordeulem  8591  oaabslem  8684  oaabs2  8686  omabslem  8687  omabs  8688  marypha2lem1  9473  ttrclselem1  9763  trcl  9766  r1val1  9824  rankuni2b  9891  rankval4  9905  rankbnd  9906  rankbnd2  9907  rankc1  9908  cfslb2n  10306  cfsmolem  10308  hsmexlem2  10465  axdc3lem2  10489  ac6  10518  wuncval2  10785  inar1  10813  tskuni  10821  grur1a  10857  fsuppmapnn0fiublem  14028  fsuppmapnn0fiub  14029  rtrclreclem4  15097  prmreclem4  16953  prmreclem5  16954  prdsval  17502  prdsbas  17504  imasaddfnlem  17575  imasvscafn  17584  imasvscaf  17586  isacs2  17698  mreacs  17703  acsfn  17704  dmcoass  18120  isacs5  18606  dprdspan  20062  dprd2dlem1  20076  dprd2d2  20079  dmdprdsplit2lem  20080  lbsextlem2  21179  lpival  21352  iunocv  21717  tgidm  23003  iunconn  23452  comppfsc  23556  txtube  23664  txcmplem2  23666  xkococnlem  23683  xkoinjcn  23711  alexsubALTlem3  24073  cnextf  24090  imasdsf1olem  24399  metnrmlem3  24897  ovolfiniun  25550  ovoliunlem2  25552  ovoliun  25554  ovoliunnul  25556  volfiniun  25596  voliunlem1  25599  volsup  25605  uniioombllem3a  25633  uniioombllem3  25634  uniioombllem4  25635  ismbf3d  25703  limciun  25944  taylfval  26415  taylf  26417  elpwiuncl  32555  disjunsn  32614  gsumpart  33043  esum2d  34074  omssubadd  34282  eulerpartlemgh  34360  eulerpartlemgs2  34362  bnj226  34727  bnj517  34878  bnj1118  34977  bnj1137  34988  cvmlift2lem12  35299  ntruni  36310  neibastop2lem  36343  filnetlem4  36364  mblfinlem2  37645  volsupnfl  37652  cnambfre  37655  sstotbnd2  37761  equivtotbnd  37765  totbndbnd  37776  prdstotbnd  37781  heiborlem1  37798  pclfinN  39883  lcfrlem4  41528  lcfrlem16  41541  lcfr  41568  oaabsb  43284  naddgeoa  43384  naddwordnexlem4  43391  iunrelexp0  43692  iunrelexpmin1  43698  iunrelexpmin2  43702  cotrcltrcl  43715  trclimalb2  43716  cotrclrcl  43732  iunconnlem2  44933  ixpssmapc  45013  ioorrnopnlem  46260  omeiunle  46473  omeiunltfirp  46475  carageniuncl  46479  caratheodorylem1  46482  caratheodorylem2  46483  hoissrrn  46505  ovnlecvr  46514  ovnsubaddlem1  46526  ovnsubadd  46528  hoissrrn2  46534  ovnlecvr2  46566  hspmbl  46585  opnvonmbllem2  46589  vonvolmbllem  46616  vonvolmbl2  46619  vonvol2  46620  iunhoiioolem  46631  iunhoiioo  46632