Theorem iuneq1 4344

Description: Equality theorem for indexed union. (Contributed by NM, 27-Jun-1998.)

Assertion

Ref	Expression
iuneq1

Distinct variable groups:   ,   ,

Proof of Theorem iuneq1

Step	Hyp	Ref	Expression
1		iunss1 4342	. . 3
2		iunss1 4342	. . 3
3	1, 2	anim12i 566	. 2
4		eqss 3518	. 2
5		eqss 3518	. 2
6	3, 4, 5	3imtr4i 266	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  C_wss 3475  U_ciun 4330

This theorem is referenced by:  iuneq1d  4355  iinvdif  4402  iununi  4415  iunsuc  4965  funiunfv  6160  onfununi  7031  iunfi  7828  rankuni2b  8292  pwsdompw  8605  ackbij1lem7  8627  r1om  8645  fictb  8646  cfsmolem  8671  ituniiun  8823  domtriomlem  8843  domtriom  8844  inar1  9174  fsum2d  13586  fsumiun  13635  ackbijnn  13640  fprod2d  13785  prmreclem5  14438  lpival  17893  fiuncmp  19904  ovolfiniun  21912  ovoliunnul  21918  finiunmbl  21954  volfiniun  21957  voliunlem1  21960  iuninc  27428  ofpreima2  27508  sigaclfu2  28121  trpredlem1  29310  trpredtr  29313  trpredmintr  29314  trpredrec  29321  neibastop2lem  30178  istotbnd3  30267  0totbnd  30269  sstotbnd2  30270  sstotbnd  30271  sstotbnd3  30272  totbndbnd  30285  prdstotbnd  30290  cntotbnd  30292  heibor  30317  iunxprg  32302  bnj548  33955  bnj554  33957  bnj594  33970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-in 3482  df-ss 3489  df-iun 4332