Theorem iunss 5009

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 4957	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 3975	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 4026	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		df-ss 3931	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3075	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3263	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3161	. . . 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 3914  ∪ ciun 4955

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 3931  df-iun 4957

This theorem is referenced by:  iunss2  5013  iunssd  5014  djussxp  5809  fiun  7921  f1iun  7922  frrlem7  8271  onfununi  8310  oawordeulem  8518  oaabslem  8611  oaabs2  8613  omabslem  8614  omabs  8615  marypha2lem1  9386  ttrclselem1  9678  trcl  9681  r1val1  9739  rankuni2b  9806  rankval4  9820  rankbnd  9821  rankbnd2  9822  rankc1  9823  cfslb2n  10221  cfsmolem  10223  hsmexlem2  10380  axdc3lem2  10404  ac6  10433  wuncval2  10700  inar1  10728  tskuni  10736  grur1a  10772  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  rtrclreclem4  15027  prmreclem4  16890  prmreclem5  16891  prdsval  17418  prdsbas  17420  imasaddfnlem  17491  imasvscafn  17500  imasvscaf  17502  isacs2  17614  mreacs  17619  acsfn  17620  dmcoass  18028  isacs5  18507  dprdspan  19959  dprd2dlem1  19973  dprd2d2  19976  dmdprdsplit2lem  19977  lbsextlem2  21069  lpival  21234  iunocv  21590  tgidm  22867  iunconn  23315  comppfsc  23419  txtube  23527  txcmplem2  23529  xkococnlem  23546  xkoinjcn  23574  alexsubALTlem3  23936  cnextf  23953  imasdsf1olem  24261  metnrmlem3  24750  ovolfiniun  25402  ovoliunlem2  25404  ovoliun  25406  ovoliunnul  25408  volfiniun  25448  voliunlem1  25451  volsup  25457  uniioombllem3a  25485  uniioombllem3  25486  uniioombllem4  25487  ismbf3d  25555  limciun  25795  taylfval  26266  taylf  26268  elpwiuncl  32456  disjunsn  32523  gsumpart  32997  esum2d  34083  omssubadd  34291  eulerpartlemgh  34369  eulerpartlemgs2  34371  bnj226  34724  bnj517  34875  bnj1118  34974  bnj1137  34985  cvmlift2lem12  35301  ntruni  36315  neibastop2lem  36348  filnetlem4  36369  mblfinlem2  37652  volsupnfl  37659  cnambfre  37662  sstotbnd2  37768  equivtotbnd  37772  totbndbnd  37783  prdstotbnd  37788  heiborlem1  37805  pclfinN  39894  lcfrlem4  41539  lcfrlem16  41552  lcfr  41579  oaabsb  43283  naddgeoa  43383  naddwordnexlem4  43390  iunrelexp0  43691  iunrelexpmin1  43697  iunrelexpmin2  43701  cotrcltrcl  43714  trclimalb2  43715  cotrclrcl  43731  iunconnlem2  44924  ixpssmapc  45067  ioorrnopnlem  46302  omeiunle  46515  omeiunltfirp  46517  carageniuncl  46521  caratheodorylem1  46524  caratheodorylem2  46525  hoissrrn  46547  ovnlecvr  46556  ovnsubaddlem1  46568  ovnsubadd  46570  hoissrrn2  46576  ovnlecvr2  46608  hspmbl  46627  opnvonmbllem2  46631  vonvolmbllem  46658  vonvolmbl2  46661  vonvol2  46662  iunhoiioolem  46673  iunhoiioo  46674  iuneq0  48807  iuneqconst2  48811  imassc  49142