Theorem uniexg 4487

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 3859	. . 3 |- ( x = A -> U. x = U. A )
2	1	eleq1d 2274	. 2 |- ( x = A -> ( U. x e. _V <-> U. A e. _V ) )
3		vex 2775	. . 3 |- x e. _V
4	3	uniex 4485	. 2 |- U. x e. _V
5	2, 4	vtoclg 2833	1 |- ( A e. V -> U. A e. _V )

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2176   _Vcvv 2772   U.cuni 3850

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-13 2178  ax-14 2179  ax-ext 2187  ax-sep 4163  ax-un 4481

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-uni 3851

This theorem is referenced by:  uniexd  4488  abnexg  4494  snnex  4496  uniexb  4521  ssonuni  4537  dmexg  4943  rnexg  4944  elxp4  5171  elxp5  5172  iotaexab  5251  relrnfvex  5596  fvexg  5597  sefvex  5599  riotaexg  5905  iunexg  6206  1stvalg  6230  2ndvalg  6231  cnvf1o  6313  brtpos2  6339  tfrlemiex  6419  tfr1onlemex  6435  tfrcllemex  6448  en1bg  6894  en1uniel  6898  fival  7074  suplocexprlem2b  7829  suplocexprlemlub  7839  wrdexb  11008  restid  13115  tgval  13127  tgvalex  13128  istopon  14518  eltg  14557  eltg2  14558  tgss2  14584  ntrval  14615  restin  14681  cnovex  14701  cnprcl2k  14711  cnptopresti  14743  cnptoprest  14744  cnptoprest2  14745  lmtopcnp  14755  txbasex  14762  uptx  14779  reldvg  15184