Theorem unissb 2524

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 2055	. . 3 |- (U.A (_ B <-> A.y(y e. U.A -> y e. B))
2		eluni 2502	. . . . . 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 1292	. . . . 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 998	. . 3 |- (A.y(y e. U.A -> y e. B) <-> A.yA.x((y e. x /\ x e. A) -> y e. B))
7		alcom 1031	. . . 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 1284	. . . . . 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 998	. . . . . 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 2055	. . . . . . 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 998	. . . 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 1647	. 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 953   e. wcel 957  E.wex 979  A.wral 1643   (_ wss 2044  U.cuni 2499

This theorem is referenced by:  uniss2 2525  ssunieq 2527  pwssb 2756  bm2.5ii 3015  ordunisssuc 3079  sbthlem1 4436  isfinite2 4532  ac6lem 4737  zorn 4780  suplem1pr 5144  suplem2pr 5145  istps5 7570  neiint 7679  neips 7687  unnei 7695  qusp 10489  fgsb 10503  fgsb2 10508  rcfpfil 10517

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-v 1809  df-in 2048  df-ss 2050  df-uni 2500

Copyright terms: Public domain