Theorem iuneq2 4332

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 4331	. . 3 |- ( A. x e. A B C_ C -> U_ x e. A B C_ U_ x e. A C )
2		ss2iun 4331	. . 3 |- ( A. x e. A C C_ B -> U_ x e. A C C_ U_ x e. A B )
3	1, 2	anim12i 564	. 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 3504	. . . 4 |- ( B = C <-> ( B C_ C /\ C C_ B ) )
5	4	ralbii 2885	. . 3 |- ( A. x e. A B = C <-> A. x e. A ( B C_ C /\ C C_ B ) )
6		r19.26 2981	. . 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 249	. 2 |- ( A. x e. A B = C <-> ( A. x e. A B C_ C /\ A. x e. A C C_ B ) )
8		eqss 3504	. 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 266	1 |- ( A. x e. A B = C -> U_ x e. A B = U_ x e. A C )

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1398   A.wral 2804   C_ wss 3461   U_ciun 4315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rex 2810  df-v 3108  df-in 3468  df-ss 3475  df-iun 4317

This theorem is referenced by:  iuneq2i  4334  iuneq2dv  4337  oa0r  7180  om0r  7181  om1r  7184  oe1m  7186  oaass  7202  oarec  7203  omass  7221  oeoalem  7237  oeoelem  7239  cardiun  8354  kmlem11  8531  iuncld  19716  comppfsc  20202  iunxdif3  27640  esum2dlem  28324  istotbnd3  30510  sstotbnd  30514  heibor  30560  iuneq12f  30815