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

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 instead of to make the theorem more general and thus shorten some proofs; obviously the universal class constant is one possible substitution for class variable . (Contributed by NM, 25-Nov-1994.)
Assertion
Ref Expression
uniexg

Proof of Theorem uniexg
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 unieq 3777 . . 3
21eleq1d 2223 . 2
3 vex 2712 . . 3
43uniex 4392 . 2
52, 4vtoclg 2769 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1332   wcel 2125  cvv 2709  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
 Copyright terms: Public domain W3C validator