Theorem uniexg 4394

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 3777	. . 3 |- ( x = A -> U. x = U. A )
2	1	eleq1d 2223	. 2 |- ( x = A -> ( U. x e. _V <-> U. A e. _V ) )
3		vex 2712	. . 3 |- x e. _V
4	3	uniex 4392	. 2 |- U. x e. _V
5	2, 4	vtoclg 2769	1 |- ( A e. V -> U. A e. _V )

Syntax hints:   -> wi 4   = wceq 1332   e. wcel 2125   _Vcvv 2709   U.cuni 3768

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 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2127  ax-14 2128  ax-ext 2136  ax-sep 4078  ax-un 4388

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-rex 2438  df-v 2711  df-uni 3769

This theorem is referenced by:  abnexg  4400  snnex  4402  uniexb  4427  ssonuni  4441  dmexg  4843  rnexg  4844  elxp4  5066  elxp5  5067  relrnfvex  5479  fvexg  5480  sefvex  5482  riotaexg  5774  iunexg  6057  1stvalg  6080  2ndvalg  6081  cnvf1o  6162  brtpos2  6188  tfrlemiex  6268  tfr1onlemex  6284  tfrcllemex  6297  en1bg  6734  en1uniel  6738  fival  6903  suplocexprlem2b  7613  suplocexprlemlub  7623  restid  12301  istopon  12350  tgval  12388  tgvalex  12389  eltg  12391  eltg2  12392  tgss2  12418  ntrval  12449  restin  12515  cnovex  12535  cnprcl2k  12545  cnptopresti  12577  cnptoprest  12578  cnptoprest2  12579  lmtopcnp  12589  txbasex  12596  uptx  12613  reldvg  12987