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  5975  iunexg  6281  1stvalg  6305  2ndvalg  6306  cnvf1o  6390  brtpos2  6417  tfrlemiex  6497  tfr1onlemex  6513  tfrcllemex  6526  en1bg  6974  en1uniel  6978  fival  7169  suplocexprlem2b  7934  suplocexprlemlub  7944  wrdexb  11126  restid  13335  tgval  13347  tgvalex  13348  istopon  14740  eltg  14779  eltg2  14780  tgss2  14806  ntrval  14837  restin  14903  cnovex  14923  cnprcl2k  14933  cnptopresti  14965  cnptoprest  14966  cnptoprest2  14967  lmtopcnp  14977  txbasex  14984  uptx  15001  reldvg  15406