Theorem uniexg 4439

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 3818	. . 3 |- ( x = A -> U. x = U. A )
2	1	eleq1d 2246	. 2 |- ( x = A -> ( U. x e. _V <-> U. A e. _V ) )
3		vex 2740	. . 3 |- x e. _V
4	3	uniex 4437	. 2 |- U. x e. _V
5	2, 4	vtoclg 2797	1 |- ( A e. V -> U. A e. _V )

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148   _Vcvv 2737   U.cuni 3809

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-un 4433

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-uni 3810

This theorem is referenced by:  uniexd  4440  abnexg  4446  snnex  4448  uniexb  4473  ssonuni  4487  dmexg  4891  rnexg  4892  elxp4  5116  elxp5  5117  relrnfvex  5533  fvexg  5534  sefvex  5536  riotaexg  5834  iunexg  6119  1stvalg  6142  2ndvalg  6143  cnvf1o  6225  brtpos2  6251  tfrlemiex  6331  tfr1onlemex  6347  tfrcllemex  6360  en1bg  6799  en1uniel  6803  fival  6968  suplocexprlem2b  7712  suplocexprlemlub  7722  restid  12698  tgval  12710  tgvalex  12711  istopon  13483  eltg  13522  eltg2  13523  tgss2  13549  ntrval  13580  restin  13646  cnovex  13666  cnprcl2k  13676  cnptopresti  13708  cnptoprest  13709  cnptoprest2  13710  lmtopcnp  13720  txbasex  13727  uptx  13744  reldvg  14118