Theorem iunss 2587

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 2055	. . . 4 |- (B (_ C <-> A.y(y e. B -> y e. C))
2	1	ralbii 1665	. . 3 |- (A.x e. A B (_ C <-> A.x e. A A.y(y e. B -> y e. C))
3		df-ral 1647	. . 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 998	. . . . 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 1284	. . . . 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 998	. . 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 1292	. . . . 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 2566	. . . . . . 7 |- (y e. U_x e. A B <-> E.x e. A y e. B)
12		df-rex 1648	. . . . . . 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 998	. . 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 1031	. . 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 2055	. . 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 953   e. wcel 957  E.wex 979  A.wral 1643  E.wrex 1644   (_ wss 2044  U_ciun 2562

This theorem is referenced by:  iunss2 2591  oawordeulem 4181  oaabslem 4244  trcl 4628  r1val1 4641  rankuni2 4673  rankval4 4685  rankbnd 4686  rankbnd2 4687  rankc1 4688  iincld 7639  cncnplem4 7737  ubthlem5 8492

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-ral 1647  df-rex 1648  df-v 1809  df-in 2048  df-ss 2050  df-iun 2564

Copyright terms: Public domain