Theorem uniexg 4369

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 3753	. . 3 |- ( x = A -> U. x = U. A )
2	1	eleq1d 2209	. 2 |- ( x = A -> ( U. x e. _V <-> U. A e. _V ) )
3		vex 2692	. . 3 |- x e. _V
4	3	uniex 4367	. 2 |- U. x e. _V
5	2, 4	vtoclg 2749	1 |- ( A e. V -> U. A e. _V )

Syntax hints:   -> wi 4   = wceq 1332   e. wcel 1481   _Vcvv 2689   U.cuni 3744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-un 4363

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-uni 3745

This theorem is referenced by:  abnexg  4375  snnex  4377  uniexb  4402  ssonuni  4412  dmexg  4811  rnexg  4812  elxp4  5034  elxp5  5035  relrnfvex  5447  fvexg  5448  sefvex  5450  riotaexg  5742  iunexg  6025  1stvalg  6048  2ndvalg  6049  cnvf1o  6130  brtpos2  6156  tfrlemiex  6236  tfr1onlemex  6252  tfrcllemex  6265  en1bg  6702  en1uniel  6706  fival  6866  suplocexprlem2b  7546  suplocexprlemlub  7556  restid  12170  istopon  12219  tgval  12257  tgvalex  12258  eltg  12260  eltg2  12261  tgss2  12287  ntrval  12318  restin  12384  cnovex  12404  cnprcl2k  12414  cnptopresti  12446  cnptoprest  12447  cnptoprest2  12448  lmtopcnp  12458  txbasex  12465  uptx  12482  reldvg  12856