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

Theorem uniexg 7456
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 4838 . . 3 (𝑥 = 𝐴 𝑥 = 𝐴)
21eleq1d 2894 . 2 (𝑥 = 𝐴 → ( 𝑥 ∈ V ↔ 𝐴 ∈ V))
3 vuniex 7455 . 2 𝑥 ∈ V
42, 3vtoclg 3565 1 (𝐴𝑉 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  Vcvv 3492   cuni 4830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-v 3494  df-uni 4831
This theorem is referenced by:  uniexd  7457  abnexg  7467  uniexb  7475  pwexr  7476  ssonuni  7490  ssonprc  7496  dmexg  7602  rnexg  7603  undefval  7931  onovuni  7968  tz7.44lem1  8030  tz7.44-3  8033  en1uniel  8569  disjen  8662  domss2  8664  fival  8864  fipwuni  8878  supexd  8905  cantnflem1  9140  dfac8clem  9446  onssnum  9454  dfac12lem1  9557  dfac12lem2  9558  fin1a2lem12  9821  hsmexlem1  9836  wrdexb  13861  restid  16695  prdsbas  16718  prdsplusg  16719  prdsmulr  16720  prdsvsca  16721  prdshom  16728  sscpwex  17073  pmtrfv  18509  istopon  21448  tgval  21491  eltg2  21494  tgss2  21523  neiptoptop  21667  restin  21702  restntr  21718  cnprest2  21826  pnrmopn  21879  cnrmnrm  21897  cmpsublem  21935  cmpsub  21936  cmpcld  21938  hausmapdom  22036  isref  22045  locfindis  22066  txbasex  22102  dfac14lem  22153  xkopt  22191  xkopjcn  22192  qtopval2  22232  elqtop  22233  fbssfi  22373  ptcmplem2  22589  cnextfval  22598  tuslem  22803  pliguhgr  28190  elpwunicl  30234  acunirnmpt2  30333  acunirnmpt2f  30334  hasheuni  31243  insiga  31295  sigagenval  31298  omsval  31450  omssubadd  31457  sibfof  31497  sitmcl  31508  kur14  32360  cvmscld  32417  madeval  33186  fobigcup  33258  hfuni  33542  isfne  33584  isfne4b  33586  fnemeet1  33611  tailfval  33617  bj-restuni2  34283  pibt2  34580  imaexALTV  35468  kelac2  39543  cnfex  41162  unidmex  41189  pwpwuni  41196  salgenval  42483  intsaluni  42489  salgenn0  42491  caragenunidm  42667  afv2ex  43290
  Copyright terms: Public domain W3C validator