Theorem uniex 2870

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

Syntax hints:   = wceq 956   e. wcel 958  Vcvv 1811  U.cuni 2503

This theorem is referenced by:  uniexg 2871  unex 2872  uniuni 2880  iunpw 2914  elxp4 3453  elxp5 3454  fvex 3732  tz7.44-3 3930  1stval 4081  2ndval 4082  fo1st 4091  fo2nd 4092  xpcomen 4439  xpmapenlem2 4497  abfii2OLD 4562  supex 4577  trcl 4645  rankuni2 4690  rankuni 4698  rankc2 4706  rankxpl 4710  rankxpsuc 4715  hta 4728  aceq3 4733  aceq6a 4741  kmlem2 4766  zorn2lem1 4788  brdom7disj 4804  brdom6disj 4805  unidom 4808  subvalt 5357  pnfxr 5493  mnfxr 5494  pnfnemnf 5536  divval 5704  flvalt 6225  revalt 6755  imvalt 6756  ref 6759  imf 6760  sumex 6981  acdc3lem 7486  acdc2lem1 7488  acdc2lem2 7489  acdc5lem1 7491  acdc5lem2 7492  acdclem 7494  infxpidmlem8 7559  eltg3t 7626  subtop 7646  sn0top 7647  distop 7649  fctopOLD 7650  cctop 7652  0vfval 8225  pjspansnt 9500  pjfn 9646  cnlnadjlem4 10003  cnlnadjlem5 10004  nmopadjle 10021  cdj3lem2 10362  hmeogrp 10538  qusp 10555

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-uni 2504

Copyright terms: Public domain