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

Theorem uniexg 6997
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 4476 . . 3 (𝑥 = 𝐴 𝑥 = 𝐴)
21eleq1d 2715 . 2 (𝑥 = 𝐴 → ( 𝑥 ∈ V ↔ 𝐴 ∈ V))
3 vuniex 6996 . 2 𝑥 ∈ V
42, 3vtoclg 3297 1 (𝐴𝑉 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  Vcvv 3231   cuni 4468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-v 3233  df-uni 4469
This theorem is referenced by:  abnexg  7006  snnexOLD  7009  uniexb  7015  pwexr  7016  ssonuni  7028  ssonprc  7034  dmexg  7139  rnexg  7140  iunexg  7185  undefval  7447  onovuni  7484  tz7.44lem1  7546  tz7.44-3  7549  en1b  8065  en1uniel  8069  disjen  8158  domss2  8160  fival  8359  fipwuni  8373  supexd  8400  cantnflem1  8624  dfac8clem  8893  onssnum  8901  dfac12lem1  9003  dfac12lem2  9004  fin1a2lem12  9271  hsmexlem1  9286  axdc2lem  9308  ttukeylem3  9371  wrdexb  13348  restid  16141  prdsbas  16164  prdsplusg  16165  prdsmulr  16166  prdsvsca  16167  prdshom  16174  sscpwex  16522  pmtrfv  17918  frgpcyg  19970  istopon  20765  tgval  20807  eltg  20809  eltg2  20810  tgss2  20839  ntrval  20888  neiptoptop  20983  neiptopnei  20984  restin  21018  neitr  21032  restntr  21034  cnpresti  21140  cnprest  21141  cnprest2  21142  lmcnp  21156  pnrmopn  21195  cnrmnrm  21213  cmpsublem  21250  cmpsub  21251  cmpcld  21253  hausmapdom  21351  isref  21360  locfindis  21381  txbasex  21417  dfac14lem  21468  uptx  21476  xkopt  21506  xkopjcn  21507  qtopval2  21547  elqtop  21548  fbssfi  21688  ptcmplem2  21904  cnextfval  21913  cnextcn  21918  tuslem  22118  isppw  24885  pliguhgr  27468  elpwunicl  29497  acunirnmpt2  29588  acunirnmpt2f  29589  hasheuni  30275  insiga  30328  sigagenval  30331  braew  30433  omsval  30483  omssubaddlem  30489  omssubadd  30490  omsmeas  30513  sibfof  30530  sitmcl  30541  isrrvv  30633  rrvmulc  30643  bnj1489  31250  kur14  31324  cvmscld  31381  bdayimaon  31968  nosupno  31974  madeval  32060  fobigcup  32132  hfuni  32416  isfne  32459  isfne4b  32461  topjoin  32485  fnemeet1  32486  tailfval  32492  bj-restuni2  33176  mbfresfi  33586  supex2g  33662  kelac2  37952  cnfex  39501  unidmex  39531  pwpwuni  39539  uniexd  39595  unirnmap  39714  stoweidlem50  40585  stoweidlem57  40592  stoweidlem59  40594  stoweidlem60  40595  fourierdlem71  40712  salgenval  40859  intsaluni  40865  intsal  40866  salgenn0  40867  caragenval  41028  omecl  41038  caragenunidm  41043  setrec1lem2  42760
  Copyright terms: Public domain W3C validator