Theorem uniexg 4441

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 3820	. . 3 |- ( x = A -> U. x = U. A )
2	1	eleq1d 2246	. 2 |- ( x = A -> ( U. x e. _V <-> U. A e. _V ) )
3		vex 2742	. . 3 |- x e. _V
4	3	uniex 4439	. 2 |- U. x e. _V
5	2, 4	vtoclg 2799	1 |- ( A e. V -> U. A e. _V )

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

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 4123  ax-un 4435

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 2741  df-uni 3812

This theorem is referenced by:  uniexd  4442  abnexg  4448  snnex  4450  uniexb  4475  ssonuni  4489  dmexg  4893  rnexg  4894  elxp4  5118  elxp5  5119  relrnfvex  5535  fvexg  5536  sefvex  5538  riotaexg  5837  iunexg  6122  1stvalg  6145  2ndvalg  6146  cnvf1o  6228  brtpos2  6254  tfrlemiex  6334  tfr1onlemex  6350  tfrcllemex  6363  en1bg  6802  en1uniel  6806  fival  6971  suplocexprlem2b  7715  suplocexprlemlub  7725  restid  12704  tgval  12716  tgvalex  12717  istopon  13598  eltg  13637  eltg2  13638  tgss2  13664  ntrval  13695  restin  13761  cnovex  13781  cnprcl2k  13791  cnptopresti  13823  cnptoprest  13824  cnptoprest2  13825  lmtopcnp  13835  txbasex  13842  uptx  13859  reldvg  14233