ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  uniexg Unicode version

Theorem uniexg 4329
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.
StepHypRef Expression
1 unieq 3713 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
21eleq1d 2184 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
3 vex 2661 . . 3  |-  x  e. 
_V
43uniex 4327 . 2  |-  U. x  e.  _V
52, 4vtoclg 2718 1  |-  ( A  e.  V  ->  U. A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1314    e. wcel 1463   _Vcvv 2658   U.cuni 3704
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-un 4323
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-rex 2397  df-v 2660  df-uni 3705
This theorem is referenced by:  abnexg  4335  snnex  4337  uniexb  4362  ssonuni  4372  dmexg  4771  rnexg  4772  elxp4  4994  elxp5  4995  relrnfvex  5405  fvexg  5406  sefvex  5408  riotaexg  5700  iunexg  5983  1stvalg  6006  2ndvalg  6007  cnvf1o  6088  brtpos2  6114  tfrlemiex  6194  tfr1onlemex  6210  tfrcllemex  6223  en1bg  6660  en1uniel  6664  fival  6824  suplocexprlem2b  7486  suplocexprlemlub  7496  restid  12026  istopon  12075  tgval  12113  tgvalex  12114  eltg  12116  eltg2  12117  tgss2  12143  ntrval  12174  restin  12240  cnovex  12260  cnprcl2k  12270  cnptopresti  12302  cnptoprest  12303  cnptoprest2  12304  lmtopcnp  12314  txbasex  12321  uptx  12338  reldvg  12700
  Copyright terms: Public domain W3C validator