Theorem uniexg 6955

Description: The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent A e. V instead of A e. _V to make the theorem more general and thus shorten some proofs; obviously the universal class constant _V is one possible substitution for class variable V. (Contributed by NM, 25-Nov-1994.)

Assertion

Ref	Expression
uniexg	|- ( A e. V -> U. A e. _V )

Proof of Theorem uniexg

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		unieq 4444	. . 3 |- ( x = A -> U. x = U. A )
2	1	eleq1d 2686	. 2 |- ( x = A -> ( U. x e. _V <-> U. A e. _V ) )
3		vuniex 6954	. 2 |- U. x e. _V
4	2, 3	vtoclg 3266	1 |- ( A e. V -> U. A e. _V )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   _Vcvv 3200   U.cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-v 3202  df-uni 4437

This theorem is referenced by:  abnexg  6964  snnexOLD  6967  uniexb  6973  pwexr  6974  ssonuni  6986  ssonprc  6992  dmexg  7097  rnexg  7098  iunexg  7143  undefval  7402  onovuni  7439  tz7.44lem1  7501  tz7.44-3  7504  en1b  8024  en1uniel  8028  disjen  8117  domss2  8119  fival  8318  fipwuni  8332  supexd  8359  cantnflem1  8586  dfac8clem  8855  onssnum  8863  dfac12lem1  8965  dfac12lem2  8966  fin1a2lem12  9233  hsmexlem1  9248  axdc2lem  9270  ttukeylem3  9333  wrdexb  13316  restid  16094  prdsbas  16117  prdsplusg  16118  prdsmulr  16119  prdsvsca  16120  prdshom  16127  sscpwex  16475  pmtrfv  17872  frgpcyg  19922  istopon  20717  tgval  20759  eltg  20761  eltg2  20762  tgss2  20791  ntrval  20840  neiptoptop  20935  neiptopnei  20936  restin  20970  neitr  20984  restntr  20986  cnpresti  21092  cnprest  21093  cnprest2  21094  lmcnp  21108  pnrmopn  21147  cnrmnrm  21165  cmpsublem  21202  cmpsub  21203  cmpcld  21205  hausmapdom  21303  isref  21312  locfindis  21333  txbasex  21369  dfac14lem  21420  uptx  21428  xkopt  21458  xkopjcn  21459  qtopval2  21499  elqtop  21500  fbssfi  21641  ptcmplem2  21857  cnextfval  21866  cnextcn  21871  tuslem  22071  isppw  24840  pliguhgr  27338  elpwunicl  29371  acunirnmpt2  29460  acunirnmpt2f  29461  hasheuni  30147  insiga  30200  sigagenval  30203  braew  30305  omsval  30355  omssubaddlem  30361  omssubadd  30362  omsmeas  30385  sibfof  30402  sitmcl  30413  isrrvv  30505  rrvmulc  30515  bnj1489  31124  kur14  31198  cvmscld  31255  bdayimaon  31843  nosupno  31849  madeval  31935  fobigcup  32007  hfuni  32291  isfne  32334  isfne4b  32336  topjoin  32360  fnemeet1  32361  tailfval  32367  bj-restuni2  33051  mbfresfi  33456  supex2g  33532  kelac2  37635  cnfex  39187  unidmex  39217  pwpwuni  39225  uniexd  39281  unirnmap  39400  stoweidlem50  40267  stoweidlem57  40274  stoweidlem59  40276  stoweidlem60  40277  fourierdlem71  40394  salgenval  40541  intsaluni  40547  intsal  40548  salgenn0  40549  caragenval  40707  omecl  40717  caragenunidm  40722  setrec1lem2  42435