Theorem uniex 2861

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

Syntax hints:   = wceq 953   e. wcel 955  Vcvv 1802  U.cuni 2493

This theorem is referenced by:  uniexg 2862  unex 2863  uniuni 2870  iunpw 2904  elxp4 3439  elxp5 3440  fvex 3717  tz7.44-3 3915  1stval 4065  2ndval 4066  fo1st 4075  fo2nd 4076  xpcomen 4419  2pwuninel 4465  xpmapenlem2 4477  abfii2 4536  supex 4551  trcl 4617  rankuni2 4662  rankuni 4670  rankc2 4678  rankxpl 4682  rankxpsuc 4687  hta 4700  aceq3 4705  aceq6a 4713  kmlem2 4738  zorn2lem1 4760  brdom7disj 4776  brdom6disj 4777  unidom 4780  subvalt 5329  pnfxr 5465  mnfxr 5466  pnfnemnf 5509  divval 5673  flvalt 6173  revalt 6686  imvalt 6687  ref 6690  imf 6691  sumex 6919  acdc3lem 7428  acdc2lem1 7430  acdc2lem2 7431  acdc5lem1 7433  acdc5lem2 7434  acdclem 7436  infxpidmlem8 7502  eltg3t 7568  subtop 7588  sn0top 7589  distop 7591  fctop 7592  cctop 7594  0vfval 8163  pjspansnt 9417  pjfn 9563  cnlnadjlem4 9918  cnlnadjlem5 9919  nmopadjle 9936  cdj3lem2 10267  hmeogrp 10425  qusp 10430

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-13 966  ax-14 967  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  ax-sep 2693  ax-un 2857

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-uni 2494

Copyright terms: Public domain