Theorem iuneq2 2582

Description: Equality theorem for indexed union.

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 2581	. . 3 |- (A.x e. A B (_ C -> U_x e. A B (_ U_x e. A C)
2		ss2iun 2581	. . 3 |- (A.x e. A C (_ B -> U_x e. A C (_ U_x e. A B)
3	1, 2	anim12i 333	. 2 |- ((A.x e. A B (_ C /\ A.x e. A C (_ B) -> (U_x e. A B (_ U_x e. A C /\ U_x e. A C (_ U_x e. A B))
4		eqss 2080	. . . 4 |- (B = C <-> (B (_ C /\ C (_ B))
5	4	ralbii 1670	. . 3 |- (A.x e. A B = C <-> A.x e. A (B (_ C /\ C (_ B))
6		r19.26 1753	. . 3 |- (A.x e. A (B (_ C /\ C (_ B) <-> (A.x e. A B (_ C /\ A.x e. A C (_ B))
7	5, 6	bitr 173	. 2 |- (A.x e. A B = C <-> (A.x e. A B (_ C /\ A.x e. A C (_ B))
8		eqss 2080	. 2 |- (U_x e. A B = U_x e. A C <-> (U_x e. A B (_ U_x e. A C /\ U_x e. A C (_ U_x e. A B))
9	3, 7, 8	3imtr4 219	1 |- (A.x e. A B = C -> U_x e. A B = U_x e. A C)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 958  A.wral 1648   (_ wss 2050  U_ciun 2570

This theorem is referenced by:  iuneq2i 2584  iuneq2dv 2586  abianfplem 3967  oa0r 4179  om0r 4180  om1r 4183  oe1m 4185  oaass 4201  oarec 4202  omass 4217  oaabs 4258  r1val3 4689  kmlem11 4785  cardiun 4870

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ral 1652  df-rex 1653  df-v 1815  df-in 2054  df-ss 2056  df-iun 2572

Copyright terms: Public domain