Theorem unissb 2518

Description: Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse.

Assertion

Ref	Expression
unissb	|- (U.A (_ B <-> A.x e. A x (_ B)

Distinct variable groups:   x,A   x,B

Proof of Theorem unissb

Step	Hyp	Ref	Expression
1		dfss2 2048	. . 3 |- (U.A (_ B <-> A.y(y e. U.A -> y e. B))
2		eluni 2496	. . . . . 6 |- (y e. U.A <-> E.x(y e. x /\ x e. A))
3	2	imbi1i 186	. . . . 5 |- ((y e. U.A -> y e. B) <-> (E.x(y e. x /\ x e. A) -> y e. B))
4		19.23v 1288	. . . . 5 |- (A.x((y e. x /\ x e. A) -> y e. B) <-> (E.x(y e. x /\ x e. A) -> y e. B))
5	3, 4	bitr4 176	. . . 4 |- ((y e. U.A -> y e. B) <-> A.x((y e. x /\ x e. A) -> y e. B))
6	5	albii 996	. . 3 |- (A.y(y e. U.A -> y e. B) <-> A.yA.x((y e. x /\ x e. A) -> y e. B))
7		alcom 1028	. . . 4 |- (A.yA.x((y e. x /\ x e. A) -> y e. B) <-> A.xA.y((y e. x /\ x e. A) -> y e. B))
8		19.21v 1280	. . . . . 6 |- (A.y(x e. A -> (y e. x -> y e. B)) <-> (x e. A -> A.y(y e. x -> y e. B)))
9		impexp 347	. . . . . . . 8 |- (((y e. x /\ x e. A) -> y e. B) <-> (y e. x -> (x e. A -> y e. B)))
10		bi2.04 160	. . . . . . . 8 |- ((y e. x -> (x e. A -> y e. B)) <-> (x e. A -> (y e. x -> y e. B)))
11	9, 10	bitr 173	. . . . . . 7 |- (((y e. x /\ x e. A) -> y e. B) <-> (x e. A -> (y e. x -> y e. B)))
12	11	albii 996	. . . . . 6 |- (A.y((y e. x /\ x e. A) -> y e. B) <-> A.y(x e. A -> (y e. x -> y e. B)))
13		dfss2 2048	. . . . . . 7 |- (x (_ B <-> A.y(y e. x -> y e. B))
14	13	imbi2i 185	. . . . . 6 |- ((x e. A -> x (_ B) <-> (x e. A -> A.y(y e. x -> y e. B)))
15	8, 12, 14	3bitr4 183	. . . . 5 |- (A.y((y e. x /\ x e. A) -> y e. B) <-> (x e. A -> x (_ B))
16	15	albii 996	. . . 4 |- (A.xA.y((y e. x /\ x e. A) -> y e. B) <-> A.x(x e. A -> x (_ B))
17	7, 16	bitr 173	. . 3 |- (A.yA.x((y e. x /\ x e. A) -> y e. B) <-> A.x(x e. A -> x (_ B))
18	1, 6, 17	3bitr 177	. 2 |- (U.A (_ B <-> A.x(x e. A -> x (_ B))
19		df-ral 1641	. 2 |- (A.x e. A x (_ B <-> A.x(x e. A -> x (_ B))
20	18, 19	bitr4 176	1 |- (U.A (_ B <-> A.x e. A x (_ B)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 951   e. wcel 955  E.wex 977  A.wral 1637   (_ wss 2037  U.cuni 2493

This theorem is referenced by:  uniss2 2519  ssunieq 2521  pwssb 2750  bm2.5ii 3009  ordunisssuc 3073  sbthlem1 4427  isfinite2 4523  ac6lem 4726  zorn 4769  suplem1pr 5133  suplem2pr 5134  istps5 7552  neiint 7660  neips 7668  unnei 7676  qusp 10430  fgsb 10444  fgsb2 10449

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-ral 1641  df-v 1803  df-in 2041  df-ss 2043  df-uni 2494

Copyright terms: Public domain