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

Theorem uniexg 4361
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 3745 . . 3 (𝑥 = 𝐴 𝑥 = 𝐴)
21eleq1d 2208 . 2 (𝑥 = 𝐴 → ( 𝑥 ∈ V ↔ 𝐴 ∈ V))
3 vex 2689 . . 3 𝑥 ∈ V
43uniex 4359 . 2 𝑥 ∈ V
52, 4vtoclg 2746 1 (𝐴𝑉 𝐴 ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1331  wcel 1480  Vcvv 2686   cuni 3736
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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-un 4355
This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-v 2688  df-uni 3737
This theorem is referenced by:  abnexg  4367  snnex  4369  uniexb  4394  ssonuni  4404  dmexg  4803  rnexg  4804  elxp4  5026  elxp5  5027  relrnfvex  5439  fvexg  5440  sefvex  5442  riotaexg  5734  iunexg  6017  1stvalg  6040  2ndvalg  6041  cnvf1o  6122  brtpos2  6148  tfrlemiex  6228  tfr1onlemex  6244  tfrcllemex  6257  en1bg  6694  en1uniel  6698  fival  6858  suplocexprlem2b  7529  suplocexprlemlub  7539  restid  12141  istopon  12190  tgval  12228  tgvalex  12229  eltg  12231  eltg2  12232  tgss2  12258  ntrval  12289  restin  12355  cnovex  12375  cnprcl2k  12385  cnptopresti  12417  cnptoprest  12418  cnptoprest2  12419  lmtopcnp  12429  txbasex  12436  uptx  12453  reldvg  12827
  Copyright terms: Public domain W3C validator