Theorem uniex 3093

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

Syntax hints:   = wceq 992   e. wcel 994  Vcvv 1857  U.cuni 2569

This theorem is referenced by:  uniexg 3094  unex 3095  uniuni 3104  iunpw 3137  elxp4 3585  elxp5 3586  fvex 3843  1stval 4142  2ndval 4143  fo1st 4152  fo2nd 4153  tz7.44-3 4231  xpcomen 4580  xpmapenlem2 4644  abfii2 4705  supex 4720  trcl 4791  rankuni2 4836  rankuni 4844  rankc2 4852  rankxpl 4856  rankxpsuc 4861  hta 4874  aceq3 4879  aceq6a 4887  kmlem2 4912  zorn2lem1 4934  brdom7disj 4950  brdom6disj 4951  unidom 4954  subval 5511  pnfxr 5647  mnfxr 5648  divvali 5856  flval 6423  reval 6956  imval 6957  ref 6960  imf 6961  sumex 7184  acdc3lem 7697  acdc2lem1 7700  acdc2lem2 7701  acdc5lem1 7703  acdc5lem2 7704  acdclem 7706  infxpidmlem8 7771  eltg3 7838  subtop 7858  sn0top 7859  distop 7861  cctop 7862  grpidvallem 8274  grpidval 8275  pjspansn 9776  pjfni 9924  cnlnadjlem4 10282  cnlnadjlem5 10283  nmopadjlei 10300  cdj3lem2 10644  toplat 10884  hmeogrp 11044  qusp 11068  ordtypelem1 11427  ordtypelem6 11432  alexsublem2 11497  neibastop1 11579  neibastop2lem4 11583  topmtcl 11586  filssufillem 11655  filssufil 11656  filcon 11665  metsstop 11909  heiborlem23 12033

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-uni 2570

Copyright terms: Public domain