Theorem uniexg 4665

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 3984	. . 3 |- ( x = A -> U. x = U. A )
2	1	eleq1d 2470	. 2 |- ( x = A -> ( U. x e. _V <-> U. A e. _V ) )
3		vex 2919	. . 3 |- x e. _V
4	3	uniex 4664	. 2 |- U. x e. _V
5	2, 4	vtoclg 2971	1 |- ( A e. V -> U. A e. _V )

Syntax hints:   -> wi 4   = wceq 1649   e. wcel 1721   _Vcvv 2916   U.cuni 3975

This theorem is referenced by:  snnex  4672  uniexb  4711  ssonuni  4726  ssonprc  4731  dmexg  5089  rnexg  5090  iunexg  5946  undefval  6505  onovuni  6563  tz7.44lem1  6622  tz7.44-3  6625  en1b  7134  disjen  7223  domss2  7225  fival  7375  fipwuni  7389  supexd  7414  cantnflem1  7601  dfac8clem  7869  onssnum  7877  dfac12lem1  7979  dfac12lem2  7980  fin1a2lem12  8247  hsmexlem1  8262  axdc2lem  8284  ttukeylem3  8347  wrdexb  11718  restid  13616  prdsbas  13635  prdsplusg  13636  prdsmulr  13637  prdsvsca  13638  prdshom  13644  sscpwex  13970  frgpcyg  16809  eltopspOLD  16938  istpsOLD  16940  istopon  16945  tgval  16975  eltg  16977  eltg2  16978  tgss2  17007  ntrval  17055  neiptoptop  17150  neiptopnei  17151  restin  17184  neitr  17198  restntr  17200  cnpresti  17306  cnprest  17307  cnprest2  17308  lmcnp  17322  pnrmopn  17361  cnrmnrm  17379  cmpsublem  17416  cmpsub  17417  cmpcld  17419  hausmapdom  17516  txbasex  17551  dfac14lem  17602  uptx  17610  xkopt  17640  xkopjcn  17641  qtopval2  17681  elqtop  17682  fbssfi  17822  ptcmplem2  18037  cnextfval  18046  cnextcn  18051  tuslem  18250  isppw  20850  hasheuni  24428  insiga  24473  sigagenval  24476  braew  24546  sibfof  24607  sitmcl  24616  isrrvv  24654  rrvmulc  24664  kur14  24855  cvmscld  24913  relexp0  25082  relexpsucr  25083  nobndlem1  25560  fobigcup  25654  hfuni  26029  mbfresfi  26152  isfne  26238  isfne4b  26240  isref  26249  locfindis  26275  topjoin  26284  fnemeet1  26285  tailfval  26291  supex2g  26329  kelac2  27031  en1uniel  27248  pmtrfv  27263  cnfex  27566  stoweidlem50  27666  stoweidlem57  27673  stoweidlem59  27675  stoweidlem60  27676  bnj1489  29131

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-v 2918  df-uni 3976