Theorem iunss 4980

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 4932	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 3954	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 3999	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		dfss2 3912	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3093	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3164	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3210	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8	7	albii 1826	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	5, 6, 8	3bitrri 298	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
10	2, 3, 9	3bitri 297	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1540   ∈ wcel 2110  {cab 2717  ∀wral 3066  ∃wrex 3067   ⊆ wss 3892  ∪ ciun 4930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-v 3433  df-in 3899  df-ss 3909  df-iun 4932

This theorem is referenced by:  iunss2  4984  iunssd  4985  djussxp  5753  fiun  7779  f1iun  7780  frrlem7  8099  wfrdmssOLD  8137  onfununi  8163  oawordeulem  8370  oaabslem  8460  oaabs2  8462  omabslem  8463  omabs  8464  marypha2lem1  9172  ttrclselem1  9461  trpredlem1  9474  trpredss  9476  trpredmintr  9478  dftrpred3g  9481  trcl  9486  r1val1  9545  rankuni2b  9612  rankval4  9626  rankbnd  9627  rankbnd2  9628  rankc1  9629  cfslb2n  10025  cfsmolem  10027  hsmexlem2  10184  axdc3lem2  10208  ac6  10237  wuncval2  10504  inar1  10532  tskuni  10540  grur1a  10576  fsuppmapnn0fiublem  13708  fsuppmapnn0fiub  13709  rtrclreclem4  14770  prmreclem4  16618  prmreclem5  16619  prdsval  17164  prdsbas  17166  imasaddfnlem  17237  imasvscafn  17246  imasvscaf  17248  isacs2  17360  mreacs  17365  acsfn  17366  dmcoass  17779  isacs5  18264  dprdspan  19628  dprd2dlem1  19642  dprd2d2  19645  dmdprdsplit2lem  19646  lbsextlem2  20419  lpival  20514  iunocv  20884  tgidm  22128  iunconn  22577  comppfsc  22681  txtube  22789  txcmplem2  22791  xkococnlem  22808  xkoinjcn  22836  alexsubALTlem3  23198  cnextf  23215  imasdsf1olem  23524  metnrmlem3  24022  ovolfiniun  24663  ovoliunlem2  24665  ovoliun  24667  ovoliunnul  24669  volfiniun  24709  voliunlem1  24712  volsup  24718  uniioombllem3a  24746  uniioombllem3  24747  uniioombllem4  24748  ismbf3d  24816  limciun  25056  taylfval  25516  taylf  25518  elpwiuncl  30872  disjunsn  30929  gsumpart  31311  esum2d  32057  omssubadd  32263  eulerpartlemgh  32341  eulerpartlemgs2  32343  bnj226  32709  bnj517  32861  bnj1118  32960  bnj1137  32971  cvmlift2lem12  33272  ntruni  34512  neibastop2lem  34545  filnetlem4  34566  mblfinlem2  35811  volsupnfl  35818  cnambfre  35821  sstotbnd2  35928  equivtotbnd  35932  totbndbnd  35943  prdstotbnd  35948  heiborlem1  35965  pclfinN  37910  lcfrlem4  39555  lcfrlem16  39568  lcfr  39595  iunrelexp0  41280  iunrelexpmin1  41286  iunrelexpmin2  41290  cotrcltrcl  41303  trclimalb2  41304  cotrclrcl  41320  iunconnlem2  42525  ixpssmapc  42592  ioorrnopnlem  43816  omeiunle  44026  omeiunltfirp  44028  carageniuncl  44032  caratheodorylem1  44035  caratheodorylem2  44036  hoissrrn  44058  ovnlecvr  44067  ovnsubaddlem1  44079  ovnsubadd  44081  hoissrrn2  44087  ovnlecvr2  44119  hspmbl  44138  opnvonmbllem2  44142  vonvolmbllem  44169  vonvolmbl2  44172  vonvol2  44173  iunhoiioolem  44184  iunhoiioo  44185