Theorem iunss 5068

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 5017	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 4037	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 4086	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		df-ss 3993	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3099	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3292	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3189	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8	7	albii 1817	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	5, 6, 8	3bitrri 298	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
10	2, 3, 9	3bitri 297	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535   ∈ wcel 2108  {cab 2717  ∀wral 3067  ∃wrex 3076   ⊆ wss 3976  ∪ ciun 5015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-ss 3993  df-iun 5017

This theorem is referenced by:  iunss2  5072  iunssd  5073  djussxp  5870  fiun  7983  f1iun  7984  frrlem7  8333  wfrdmssOLD  8371  onfununi  8397  oawordeulem  8610  oaabslem  8703  oaabs2  8705  omabslem  8706  omabs  8707  marypha2lem1  9504  ttrclselem1  9794  trcl  9797  r1val1  9855  rankuni2b  9922  rankval4  9936  rankbnd  9937  rankbnd2  9938  rankc1  9939  cfslb2n  10337  cfsmolem  10339  hsmexlem2  10496  axdc3lem2  10520  ac6  10549  wuncval2  10816  inar1  10844  tskuni  10852  grur1a  10888  fsuppmapnn0fiublem  14041  fsuppmapnn0fiub  14042  rtrclreclem4  15110  prmreclem4  16966  prmreclem5  16967  prdsval  17515  prdsbas  17517  imasaddfnlem  17588  imasvscafn  17597  imasvscaf  17599  isacs2  17711  mreacs  17716  acsfn  17717  dmcoass  18133  isacs5  18618  dprdspan  20071  dprd2dlem1  20085  dprd2d2  20088  dmdprdsplit2lem  20089  lbsextlem2  21184  lpival  21357  iunocv  21722  tgidm  23008  iunconn  23457  comppfsc  23561  txtube  23669  txcmplem2  23671  xkococnlem  23688  xkoinjcn  23716  alexsubALTlem3  24078  cnextf  24095  imasdsf1olem  24404  metnrmlem3  24902  ovolfiniun  25555  ovoliunlem2  25557  ovoliun  25559  ovoliunnul  25561  volfiniun  25601  voliunlem1  25604  volsup  25610  uniioombllem3a  25638  uniioombllem3  25639  uniioombllem4  25640  ismbf3d  25708  limciun  25949  taylfval  26418  taylf  26420  elpwiuncl  32557  disjunsn  32616  gsumpart  33038  esum2d  34057  omssubadd  34265  eulerpartlemgh  34343  eulerpartlemgs2  34345  bnj226  34710  bnj517  34861  bnj1118  34960  bnj1137  34971  cvmlift2lem12  35282  ntruni  36293  neibastop2lem  36326  filnetlem4  36347  mblfinlem2  37618  volsupnfl  37625  cnambfre  37628  sstotbnd2  37734  equivtotbnd  37738  totbndbnd  37749  prdstotbnd  37754  heiborlem1  37771  pclfinN  39857  lcfrlem4  41502  lcfrlem16  41515  lcfr  41542  oaabsb  43256  naddgeoa  43356  naddwordnexlem4  43363  iunrelexp0  43664  iunrelexpmin1  43670  iunrelexpmin2  43674  cotrcltrcl  43687  trclimalb2  43688  cotrclrcl  43704  iunconnlem2  44906  ixpssmapc  44975  ioorrnopnlem  46225  omeiunle  46438  omeiunltfirp  46440  carageniuncl  46444  caratheodorylem1  46447  caratheodorylem2  46448  hoissrrn  46470  ovnlecvr  46479  ovnsubaddlem1  46491  ovnsubadd  46493  hoissrrn2  46499  ovnlecvr2  46531  hspmbl  46550  opnvonmbllem2  46554  vonvolmbllem  46581  vonvolmbl2  46584  vonvol2  46585  iunhoiioolem  46596  iunhoiioo  46597