Theorem uniexg 4536

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 3902	. . 3 |- ( x = A -> U. x = U. A )
2	1	eleq1d 2300	. 2 |- ( x = A -> ( U. x e. _V <-> U. A e. _V ) )
3		vex 2805	. . 3 |- x e. _V
4	3	uniex 4534	. 2 |- U. x e. _V
5	2, 4	vtoclg 2864	1 |- ( A e. V -> U. A e. _V )

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202   _Vcvv 2802   U.cuni 3893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-un 4530

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-uni 3894

This theorem is referenced by:  uniexd  4537  abnexg  4543  snnex  4545  uniexb  4570  ssonuni  4586  dmexg  4996  rnexg  4997  elxp4  5224  elxp5  5225  iotaexab  5305  relrnfvex  5657  fvexg  5658  sefvex  5660  riotaexg  5974  iunexg  6280  1stvalg  6304  2ndvalg  6305  cnvf1o  6389  brtpos2  6416  tfrlemiex  6496  tfr1onlemex  6512  tfrcllemex  6525  en1bg  6973  en1uniel  6977  fival  7168  suplocexprlem2b  7933  suplocexprlemlub  7943  wrdexb  11124  restid  13332  tgval  13344  tgvalex  13345  istopon  14736  eltg  14775  eltg2  14776  tgss2  14802  ntrval  14833  restin  14899  cnovex  14919  cnprcl2k  14929  cnptopresti  14961  cnptoprest  14962  cnptoprest2  14963  lmtopcnp  14973  txbasex  14980  uptx  14997  reldvg  15402