Theorem uniexg 4437

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 3817	. . 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 4435	. 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 3808

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 4119  ax-un 4431

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 3809

This theorem is referenced by:  uniexd  4438  abnexg  4444  snnex  4446  uniexb  4471  ssonuni  4485  dmexg  4888  rnexg  4889  elxp4  5113  elxp5  5114  relrnfvex  5530  fvexg  5531  sefvex  5533  riotaexg  5830  iunexg  6115  1stvalg  6138  2ndvalg  6139  cnvf1o  6221  brtpos2  6247  tfrlemiex  6327  tfr1onlemex  6343  tfrcllemex  6356  en1bg  6795  en1uniel  6799  fival  6964  suplocexprlem2b  7708  suplocexprlemlub  7718  restid  12685  istopon  13293  tgval  13331  tgvalex  13332  eltg  13334  eltg2  13335  tgss2  13361  ntrval  13392  restin  13458  cnovex  13478  cnprcl2k  13488  cnptopresti  13520  cnptoprest  13521  cnptoprest2  13522  lmtopcnp  13532  txbasex  13539  uptx  13556  reldvg  13930