Theorem uniex 1947

Description: The ZF Axiom of Union in class notation. This says that if A is a set i.e. A e. V, then the union of A is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16.

Hypothesis

Ref	Expression
uniex.1	|- A e. V

Assertion

Ref	Expression
uniex	|- U.A e. V

Proof of Theorem uniex

Step	Hyp	Ref	Expression
1		uniex.1	. 2 |- A e. V
2		unieq 1927	. . 3 |- (z = A -> U.z = U.A)
3	2	eleq1d 1155	. 2 |- (z = A -> (U.z e. V <-> U.A e. V))
4		axun 1081	. . . . . 6 |- E.xA.y(E.x(y e. x /\ x e. z) -> y e. x)
5		eluni 1922	. . . . . . . . 9 |- (y e. U.z <-> E.x(y e. x /\ x e. z))
6	5	imbi1i 161	. . . . . . . 8 |- ((y e. U.z -> y e. x) <-> (E.x(y e. x /\ x e. z) -> y e. x))
7	6	bial 695	. . . . . . 7 |- (A.y(y e. U.z -> y e. x) <-> A.y(E.x(y e. x /\ x e. z) -> y e. x))
8	7	biex 733	. . . . . 6 |- (E.xA.y(y e. U.z -> y e. x) <-> E.xA.y(E.x(y e. x /\ x e. z) -> y e. x))
9	4, 8	mpbir 165	. . . . 5 |- E.xA.y(y e. U.z -> y e. x)
10	9	bm1.3ii 1481	. . . 4 |- E.xA.y(y e. x <-> y e. U.z)
11		dfcleq 1098	. . . . 5 |- (x = U.z <-> A.y(y e. x <-> y e. U.z))
12	11	biex 733	. . . 4 |- (E.x x = U.z <-> E.xA.y(y e. x <-> y e. U.z))
13	10, 12	mpbir 165	. . 3 |- E.x x = U.z
14	13	issetri 1353	. 2 |- U.z e. V
15	1, 3, 14	vtocl 1378	1 |- U.A e. V

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196  A.wal 672  E.wex 678   e. wel 803   = wceq 1091   e. wcel 1092  Vcvv 1348  U.cuni 1919

This theorem is referenced by:  uniexg 1948  unex 1949  iunpw 2040  supex 2157  elxp4 2640  elxp5 2641  fvex 2838  iunex 2914  tz7.44-3 2968  1stval 3089  2ndval 3090  fo1st 3094  fo2nd 3095  xpcomen 3343  xpdom2 3345  xpmapenlem2 3392  xpmapenlem4 3394  trcl 3489  rankuni 3533  aceq3 3556  aceq6a 3564  kmlem2 3581  zornlem1 3603  hta 3619  subval 4134  divval 4217  flvalt 4623  revalt 4794  imvalt 4795  infxpidmlem8 4940  pjfn 5586

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-uni 1920

metamath.org