Theorem iunss 5004

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 4953	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 3972	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 4023	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		df-ss 3928	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3075	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3261	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3160	. . . 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 3911  ∪ ciun 4951

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 3928  df-iun 4953

This theorem is referenced by:  iunss2  5008  iunssd  5009  djussxp  5799  fiun  7901  f1iun  7902  frrlem7  8248  onfununi  8287  oawordeulem  8495  oaabslem  8588  oaabs2  8590  omabslem  8591  omabs  8592  marypha2lem1  9362  ttrclselem1  9654  trcl  9657  r1val1  9715  rankuni2b  9782  rankval4  9796  rankbnd  9797  rankbnd2  9798  rankc1  9799  cfslb2n  10197  cfsmolem  10199  hsmexlem2  10356  axdc3lem2  10380  ac6  10409  wuncval2  10676  inar1  10704  tskuni  10712  grur1a  10748  fsuppmapnn0fiublem  13931  fsuppmapnn0fiub  13932  rtrclreclem4  15003  prmreclem4  16866  prmreclem5  16867  prdsval  17394  prdsbas  17396  imasaddfnlem  17467  imasvscafn  17476  imasvscaf  17478  isacs2  17594  mreacs  17599  acsfn  17600  dmcoass  18008  isacs5  18489  dprdspan  19943  dprd2dlem1  19957  dprd2d2  19960  dmdprdsplit2lem  19961  lbsextlem2  21101  lpival  21266  iunocv  21623  tgidm  22900  iunconn  23348  comppfsc  23452  txtube  23560  txcmplem2  23562  xkococnlem  23579  xkoinjcn  23607  alexsubALTlem3  23969  cnextf  23986  imasdsf1olem  24294  metnrmlem3  24783  ovolfiniun  25435  ovoliunlem2  25437  ovoliun  25439  ovoliunnul  25441  volfiniun  25481  voliunlem1  25484  volsup  25490  uniioombllem3a  25518  uniioombllem3  25519  uniioombllem4  25520  ismbf3d  25588  limciun  25828  taylfval  26299  taylf  26301  bdayle  27865  elpwiuncl  32506  disjunsn  32573  gsumpart  33040  esum2d  34076  omssubadd  34284  eulerpartlemgh  34362  eulerpartlemgs2  34364  bnj226  34717  bnj517  34868  bnj1118  34967  bnj1137  34978  cvmlift2lem12  35294  ntruni  36308  neibastop2lem  36341  filnetlem4  36362  mblfinlem2  37645  volsupnfl  37652  cnambfre  37655  sstotbnd2  37761  equivtotbnd  37765  totbndbnd  37776  prdstotbnd  37781  heiborlem1  37798  pclfinN  39887  lcfrlem4  41532  lcfrlem16  41545  lcfr  41572  oaabsb  43276  naddgeoa  43376  naddwordnexlem4  43383  iunrelexp0  43684  iunrelexpmin1  43690  iunrelexpmin2  43694  cotrcltrcl  43707  trclimalb2  43708  cotrclrcl  43724  iunconnlem2  44917  ixpssmapc  45060  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  48800  iuneqconst2  48804  imassc  49135