Theorem iunss 4994

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 4943	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 3964	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 4015	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		df-ss 3920	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3075	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3255	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3156	. . . 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 206  ∀wal 1538   ∈ wcel 2109  {cab 2707  ∀wral 3044  ∃wrex 3053   ⊆ wss 3903  ∪ ciun 4941

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-ss 3920  df-iun 4943

This theorem is referenced by:  iunss2  4998  iunssd  4999  djussxp  5788  fiun  7878  f1iun  7879  frrlem7  8225  onfununi  8264  oawordeulem  8472  oaabslem  8565  oaabs2  8567  omabslem  8568  omabs  8569  marypha2lem1  9325  ttrclselem1  9621  trcl  9624  r1val1  9682  rankuni2b  9749  rankval4  9763  rankbnd  9764  rankbnd2  9765  rankc1  9766  cfslb2n  10162  cfsmolem  10164  hsmexlem2  10321  axdc3lem2  10345  ac6  10374  wuncval2  10641  inar1  10669  tskuni  10677  grur1a  10713  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  rtrclreclem4  14968  prmreclem4  16831  prmreclem5  16832  prdsval  17359  prdsbas  17361  imasaddfnlem  17432  imasvscafn  17441  imasvscaf  17443  isacs2  17559  mreacs  17564  acsfn  17565  dmcoass  17973  isacs5  18454  dprdspan  19908  dprd2dlem1  19922  dprd2d2  19925  dmdprdsplit2lem  19926  lbsextlem2  21066  lpival  21231  iunocv  21588  tgidm  22865  iunconn  23313  comppfsc  23417  txtube  23525  txcmplem2  23527  xkococnlem  23544  xkoinjcn  23572  alexsubALTlem3  23934  cnextf  23951  imasdsf1olem  24259  metnrmlem3  24748  ovolfiniun  25400  ovoliunlem2  25402  ovoliun  25404  ovoliunnul  25406  volfiniun  25446  voliunlem1  25449  volsup  25455  uniioombllem3a  25483  uniioombllem3  25484  uniioombllem4  25485  ismbf3d  25553  limciun  25793  taylfval  26264  taylf  26266  bdayle  27830  elpwiuncl  32471  disjunsn  32538  gsumpart  33011  esum2d  34066  omssubadd  34274  eulerpartlemgh  34352  eulerpartlemgs2  34354  bnj226  34707  bnj517  34858  bnj1118  34957  bnj1137  34968  tz9.1regs  35073  cvmlift2lem12  35297  ntruni  36311  neibastop2lem  36344  filnetlem4  36365  mblfinlem2  37648  volsupnfl  37655  cnambfre  37658  sstotbnd2  37764  equivtotbnd  37768  totbndbnd  37779  prdstotbnd  37784  heiborlem1  37801  pclfinN  39889  lcfrlem4  41534  lcfrlem16  41547  lcfr  41574  oaabsb  43277  naddgeoa  43377  naddwordnexlem4  43384  iunrelexp0  43685  iunrelexpmin1  43691  iunrelexpmin2  43695  cotrcltrcl  43708  trclimalb2  43709  cotrclrcl  43725  iunconnlem2  44918  ixpssmapc  45061  ioorrnopnlem  46295  omeiunle  46508  omeiunltfirp  46510  carageniuncl  46514  caratheodorylem1  46517  caratheodorylem2  46518  hoissrrn  46540  ovnlecvr  46549  ovnsubaddlem1  46561  ovnsubadd  46563  hoissrrn2  46569  ovnlecvr2  46601  hspmbl  46620  opnvonmbllem2  46624  vonvolmbllem  46651  vonvolmbl2  46654  vonvol2  46655  iunhoiioolem  46666  iunhoiioo  46667  iuneq0  48813  iuneqconst2  48817  imassc  49148