Theorem iunss 2591

Description: Subset theorem for an indexed union.

Assertion

Ref	Expression
iunss	|- (U_x e. A B (_ C <-> A.x e. A B (_ C)

Distinct variable group:   x,C

Proof of Theorem iunss

Step	Hyp	Ref	Expression
1		dfss2 2058	. . . 4 |- (B (_ C <-> A.y(y e. B -> y e. C))
2	1	ralbii 1667	. . 3 |- (A.x e. A B (_ C <-> A.x e. A A.y(y e. B -> y e. C))
3		df-ral 1649	. . 3 |- (A.x e. A A.y(y e. B -> y e. C) <-> A.x(x e. A -> A.y(y e. B -> y e. C)))
4		impexp 347	. . . . . 6 |- (((x e. A /\ y e. B) -> y e. C) <-> (x e. A -> (y e. B -> y e. C)))
5	4	albii 999	. . . . 5 |- (A.y((x e. A /\ y e. B) -> y e. C) <-> A.y(x e. A -> (y e. B -> y e. C)))
6		19.21v 1285	. . . . 5 |- (A.y(x e. A -> (y e. B -> y e. C)) <-> (x e. A -> A.y(y e. B -> y e. C)))
7	5, 6	bitr2 174	. . . 4 |- ((x e. A -> A.y(y e. B -> y e. C)) <-> A.y((x e. A /\ y e. B) -> y e. C))
8	7	albii 999	. . 3 |- (A.x(x e. A -> A.y(y e. B -> y e. C)) <-> A.xA.y((x e. A /\ y e. B) -> y e. C))
9	2, 3, 8	3bitr 177	. 2 |- (A.x e. A B (_ C <-> A.xA.y((x e. A /\ y e. B) -> y e. C))
10		19.23v 1293	. . . . 5 |- (A.x((x e. A /\ y e. B) -> y e. C) <-> (E.x(x e. A /\ y e. B) -> y e. C))
11		eliun 2570	. . . . . . 7 |- (y e. U_x e. A B <-> E.x e. A y e. B)
12		df-rex 1650	. . . . . . 7 |- (E.x e. A y e. B <-> E.x(x e. A /\ y e. B))
13	11, 12	bitr 173	. . . . . 6 |- (y e. U_x e. A B <-> E.x(x e. A /\ y e. B))
14	13	imbi1i 186	. . . . 5 |- ((y e. U_x e. A B -> y e. C) <-> (E.x(x e. A /\ y e. B) -> y e. C))
15	10, 14	bitr4 176	. . . 4 |- (A.x((x e. A /\ y e. B) -> y e. C) <-> (y e. U_x e. A B -> y e. C))
16	15	albii 999	. . 3 |- (A.yA.x((x e. A /\ y e. B) -> y e. C) <-> A.y(y e. U_x e. A B -> y e. C))
17		alcom 1032	. . 3 |- (A.xA.y((x e. A /\ y e. B) -> y e. C) <-> A.yA.x((x e. A /\ y e. B) -> y e. C))
18		dfss2 2058	. . 3 |- (U_x e. A B (_ C <-> A.y(y e. U_x e. A B -> y e. C))
19	16, 17, 18	3bitr4 183	. 2 |- (A.xA.y((x e. A /\ y e. B) -> y e. C) <-> U_x e. A B (_ C)
20	9, 19	bitr2 174	1 |- (U_x e. A B (_ C <-> A.x e. A B (_ C)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 954   e. wcel 958  E.wex 980  A.wral 1645  E.wrex 1646   (_ wss 2047  U_ciun 2566

This theorem is referenced by:  iunss2 2595  oawordeulem 4188  oaabslem 4251  trcl 4645  r1val1 4658  rankuni2 4690  rankval4 4702  rankbnd 4703  rankbnd2 4704  rankc1 4705  iincld 7679  cncnplem4 7777  ubthlem5 8533

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ral 1649  df-rex 1650  df-v 1812  df-in 2051  df-ss 2053  df-iun 2568

Copyright terms: Public domain