MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uniexg Structured version   Visualization version   GIF version

Theorem uniexg 7450
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 𝐴 ∈ 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 𝑉. (Contributed by NM, 25-Nov-1994.)
Assertion
Ref Expression
uniexg (𝐴𝑉 𝐴 ∈ V)

Proof of Theorem uniexg
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 unieq 4814 . . 3 (𝑥 = 𝐴 𝑥 = 𝐴)
21eleq1d 2877 . 2 (𝑥 = 𝐴 → ( 𝑥 ∈ V ↔ 𝐴 ∈ V))
3 vuniex 7449 . 2 𝑥 ∈ V
42, 3vtoclg 3518 1 (𝐴𝑉 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2112  Vcvv 3444   cuni 4803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773  ax-sep 5170  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901  df-uni 4804
This theorem is referenced by:  uniex  7451  uniexd  7452  abnexg  7462  uniexb  7470  pwexr  7471  ssonuni  7485  ssonprc  7491  dmexg  7598  rnexg  7599  undefval  7929  onovuni  7966  tz7.44lem1  8028  tz7.44-3  8031  en1uniel  8568  disjen  8662  domss2  8664  fival  8864  fipwuni  8878  supexd  8905  cantnflem1  9140  dfac8clem  9447  onssnum  9455  dfac12lem1  9558  dfac12lem2  9559  fin1a2lem12  9826  hsmexlem1  9841  wrdexb  13872  restid  16702  prdsbas  16725  prdsplusg  16726  prdsmulr  16727  prdsvsca  16728  prdshom  16735  sscpwex  17080  pmtrfv  18575  istopon  21520  tgval  21563  eltg2  21566  tgss2  21595  neiptoptop  21739  restin  21774  restntr  21790  cnprest2  21898  pnrmopn  21951  cnrmnrm  21969  cmpsublem  22007  cmpsub  22008  cmpcld  22010  hausmapdom  22108  isref  22117  locfindis  22138  txbasex  22174  dfac14lem  22225  xkopt  22263  xkopjcn  22264  qtopval2  22304  elqtop  22305  fbssfi  22445  ptcmplem2  22661  cnextfval  22670  tuslem  22876  pliguhgr  28272  acunirnmpt2  30426  acunirnmpt2f  30427  ist0cld  31186  hasheuni  31452  insiga  31504  sigagenval  31507  omsval  31659  omssubadd  31666  sibfof  31706  sitmcl  31717  kur14  32571  cvmscld  32628  madeval  33397  fobigcup  33469  hfuni  33753  isfne  33795  isfne4b  33797  fnemeet1  33822  tailfval  33828  bj-restuni2  34508  pibt2  34829  imaexALTV  35740  kelac2  39996  cnfex  41644  unidmex  41671  pwpwuni  41678  salgenval  42950  intsaluni  42956  salgenn0  42958  caragenunidm  43134  afv2ex  43757
  Copyright terms: Public domain W3C validator