Theorem iuneq2 4308

Description: Equality theorem for indexed union. (Contributed by NM, 22-Oct-2003.)

Assertion

Ref	Expression
iuneq2	|- ( A. x e. A B = C -> U_ x e. A B = U_ x e. A C )

Proof of Theorem iuneq2

Step	Hyp	Ref	Expression
1		ss2iun 4307	. . 3 |- ( A. x e. A B C_ C -> U_ x e. A B C_ U_ x e. A C )
2		ss2iun 4307	. . 3 |- ( A. x e. A C C_ B -> U_ x e. A C C_ U_ x e. A B )
3	1, 2	anim12i 574	. 2 |- ( ( A. x e. A B C_ C /\ A. x e. A C C_ B ) -> ( U_ x e. A B C_ U_ x e. A C /\ U_ x e. A C C_ U_ x e. A B ) )
4		eqss 3458	. . . 4 |- ( B = C <-> ( B C_ C /\ C C_ B ) )
5	4	ralbii 2830	. . 3 |- ( A. x e. A B = C <-> A. x e. A ( B C_ C /\ C C_ B ) )
6		r19.26 2928	. . 3 |- ( A. x e. A ( B C_ C /\ C C_ B ) <-> ( A. x e. A B C_ C /\ A. x e. A C C_ B ) )
7	5, 6	bitri 257	. 2 |- ( A. x e. A B = C <-> ( A. x e. A B C_ C /\ A. x e. A C C_ B ) )
8		eqss 3458	. 2 |- ( U_ x e. A B = U_ x e. A C <-> ( U_ x e. A B C_ U_ x e. A C /\ U_ x e. A C C_ U_ x e. A B ) )
9	3, 7, 8	3imtr4i 274	1 |- ( A. x e. A B = C -> U_ x e. A B = U_ x e. A C )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1454   A.wral 2748   C_ wss 3415   U_ciun 4291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-rex 2754  df-v 3058  df-in 3422  df-ss 3429  df-iun 4293

This theorem is referenced by:  iuneq2i  4310  iuneq2dv  4313  oa0r  7265  om0r  7266  om1r  7269  oe1m  7271  oaass  7287  oarec  7288  omass  7306  oeoalem  7322  oeoelem  7324  cardiun  8441  kmlem11  8615  iuncld  20108  comppfsc  20595  iunxdif3  28223  esum2dlem  28961  istotbnd3  32147  sstotbnd  32151  heibor  32197  iuneq12f  32451  cnvtrclfv  36360  iuneq2df  37419