Theorem uniexg 6366

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 4087	. . 3 |- ( x = A -> U. x = U. A )
2	1	eleq1d 2499	. 2 |- ( x = A -> ( U. x e. _V <-> U. A e. _V ) )
3		vex 2965	. . 3 |- x e. _V
4	3	uniex 6365	. 2 |- U. x e. _V
5	2, 4	vtoclg 3019	1 |- ( A e. V -> U. A e. _V )

Syntax hints:   -> wi 4   = wceq 1362   e. wcel 1755   _Vcvv 2962   U.cuni 4079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-un 6361

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-v 2964  df-uni 4080

This theorem is referenced by:  snnex  6371  uniexb  6375  ssonuni  6387  ssonprc  6392  dmexg  6498  rnexg  6499  iunexg  6542  undefval  6781  onovuni  6789  tz7.44lem1  6847  tz7.44-3  6850  en1b  7365  en1uniel  7369  disjen  7456  domss2  7458  fival  7650  fipwuni  7664  supexd  7691  cantnflem1  7885  cantnflem1OLD  7908  dfac8clem  8190  onssnum  8198  dfac12lem1  8300  dfac12lem2  8301  fin1a2lem12  8568  hsmexlem1  8583  axdc2lem  8605  ttukeylem3  8668  wrdexb  12228  restid  14354  prdsbas  14377  prdsplusg  14378  prdsmulr  14379  prdsvsca  14380  prdshom  14387  sscpwex  14710  pmtrfv  15937  frgpcyg  17847  eltopspOLD  18364  istpsOLD  18366  istopon  18371  tgval  18401  eltg  18403  eltg2  18404  tgss2  18433  ntrval  18481  neiptoptop  18576  neiptopnei  18577  restin  18611  neitr  18625  restntr  18627  cnpresti  18733  cnprest  18734  cnprest2  18735  lmcnp  18749  pnrmopn  18788  cnrmnrm  18806  cmpsublem  18843  cmpsub  18844  cmpcld  18846  bwthOLD  18855  hausmapdom  18945  txbasex  18980  dfac14lem  19031  uptx  19039  xkopt  19069  xkopjcn  19070  qtopval2  19110  elqtop  19111  fbssfi  19251  ptcmplem2  19466  cnextfval  19475  cnextcn  19480  tuslem  19683  isppw  22336  hasheuni  26387  insiga  26433  sigagenval  26436  braew  26511  sibfof  26573  isrrvv  26673  rrvmulc  26683  kur14  26951  cvmscld  27009  relexp0  27177  relexpsucr  27178  nobndlem1  27679  fobigcup  27777  hfuni  28068  mbfresfi  28279  isfne  28381  isfne4b  28383  isref  28392  locfindis  28418  topjoin  28427  fnemeet1  28428  tailfval  28434  supex2g  28472  kelac2  29260  cnfex  29592  stoweidlem50  29688  stoweidlem57  29695  stoweidlem59  29697  stoweidlem60  29698  bnj1489  31746