Theorem uniex 2865

Description: The Axiom of Union in class notation. This says that if A is a set i.e. A e. V (see isset 1810), 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 2505	. . 3 |- (x = A -> U.x = U.A)
3	2	eleq1d 1537	. 2 |- (x = A -> (U.x e. V <-> U.A e. V))
4		uniex2 2864	. . 3 |- E.y y = U.x
5	4	issetri 1812	. 2 |- U.x e. V
6	1, 3, 5	vtocl 1838	1 |- U.A e. V

Syntax hints:   = wceq 954   e. wcel 956  Vcvv 1807  U.cuni 2498

This theorem is referenced by:  uniexg 2866  unex 2867  uniuni 2875  iunpw 2909  elxp4 3445  elxp5 3446  fvex 3723  tz7.44-3 3921  1stval 4071  2ndval 4072  fo1st 4081  fo2nd 4082  xpcomen 4425  xpmapenlem2 4483  abfii2 4542  supex 4557  trcl 4625  rankuni2 4670  rankuni 4678  rankc2 4686  rankxpl 4690  rankxpsuc 4695  hta 4708  aceq3 4713  aceq6a 4721  kmlem2 4746  zorn2lem1 4768  brdom7disj 4784  brdom6disj 4785  unidom 4788  subvalt 5337  pnfxr 5473  mnfxr 5474  pnfnemnf 5517  divval 5681  flvalt 6181  revalt 6694  imvalt 6695  ref 6698  imf 6699  sumex 6927  acdc3lem 7436  acdc2lem1 7438  acdc2lem2 7439  acdc5lem1 7441  acdc5lem2 7442  acdclem 7444  infxpidmlem8 7510  eltg3t 7576  subtop 7596  sn0top 7597  distop 7599  fctop 7600  cctop 7602  0vfval 8177  pjspansnt 9440  pjfn 9586  cnlnadjlem4 9941  cnlnadjlem5 9942  nmopadjle 9959  cdj3lem2 10296  hmeogrp 10461  qusp 10466

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-un 2861

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-uni 2499

Copyright terms: Public domain