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

Theorem uniexg 6853
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 4380 . . 3 (𝑥 = 𝐴 𝑥 = 𝐴)
21eleq1d 2672 . 2 (𝑥 = 𝐴 → ( 𝑥 ∈ V ↔ 𝐴 ∈ V))
3 vuniex 6852 . 2 𝑥 ∈ V
42, 3vtoclg 3239 1 (𝐴𝑉 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977  Vcvv 3173   cuni 4372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-v 3175  df-uni 4373
This theorem is referenced by:  snnex  6862  uniexb  6866  ssonuni  6878  ssonprc  6884  dmexg  6989  rnexg  6990  iunexg  7035  undefval  7289  onovuni  7326  tz7.44lem1  7388  tz7.44-3  7391  en1b  7910  en1uniel  7914  disjen  8002  domss2  8004  fival  8201  fipwuni  8215  supexd  8242  cantnflem1  8469  dfac8clem  8738  onssnum  8746  dfac12lem1  8848  dfac12lem2  8849  fin1a2lem12  9116  hsmexlem1  9131  axdc2lem  9153  ttukeylem3  9216  wrdexb  13171  restid  15917  prdsbas  15940  prdsplusg  15941  prdsmulr  15942  prdsvsca  15943  prdshom  15950  sscpwex  16298  pmtrfv  17695  frgpcyg  19741  istopon  20540  tgval  20570  eltg  20572  eltg2  20573  tgss2  20602  ntrval  20650  neiptoptop  20745  neiptopnei  20746  restin  20780  neitr  20794  restntr  20796  cnpresti  20902  cnprest  20903  cnprest2  20904  lmcnp  20918  pnrmopn  20957  cnrmnrm  20975  cmpsublem  21012  cmpsub  21013  cmpcld  21015  hausmapdom  21113  isref  21122  locfindis  21143  txbasex  21179  dfac14lem  21230  uptx  21238  xkopt  21268  xkopjcn  21269  qtopval2  21309  elqtop  21310  fbssfi  21451  ptcmplem2  21667  cnextfval  21676  cnextcn  21681  tuslem  21881  isppw  24640  elpwunicl  28754  acunirnmpt2  28842  acunirnmpt2f  28843  hasheuni  29474  insiga  29527  sigagenval  29530  braew  29632  omsval  29682  omssubaddlem  29688  omssubadd  29689  omsmeas  29712  sibfof  29729  sitmcl  29740  isrrvv  29832  rrvmulc  29842  bnj1489  30378  kur14  30452  cvmscld  30509  nobndlem1  31091  fobigcup  31177  hfuni  31461  isfne  31504  isfne4b  31506  topjoin  31530  fnemeet1  31531  tailfval  31537  bj-restuni2  32232  bj-xnex  32245  mbfresfi  32626  supex2g  32702  kelac2  36653  cnfex  38210  unidmex  38242  pwpwuni  38250  uniexd  38310  unirnmap  38395  stoweidlem50  38943  stoweidlem57  38950  stoweidlem59  38952  stoweidlem60  38953  fourierdlem71  39070  salgenval  39217  intsaluni  39223  intsal  39224  salgenn0  39225  caragenval  39383  omecl  39393  caragenunidm  39398  setrec1lem2  42234
  Copyright terms: Public domain W3C validator