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

Theorem uniexg 4203
 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 3617 . . 3 (𝑥 = 𝐴 𝑥 = 𝐴)
21eleq1d 2122 . 2 (𝑥 = 𝐴 → ( 𝑥 ∈ V ↔ 𝐴 ∈ V))
3 vex 2577 . . 3 𝑥 ∈ V
43uniex 4202 . 2 𝑥 ∈ V
52, 4vtoclg 2630 1 (𝐴𝑉 𝐴 ∈ V)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1259   ∈ wcel 1409  Vcvv 2574  ∪ cuni 3608 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3903  ax-un 4198 This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-rex 2329  df-v 2576  df-uni 3609 This theorem is referenced by:  snnex  4209  uniexb  4233  ssonuni  4242  dmexg  4624  rnexg  4625  elxp4  4836  elxp5  4837  relrnfvex  5221  fvexg  5222  sefvex  5224  riotaexg  5500  iunexg  5774  1stvalg  5797  2ndvalg  5798  cnvf1o  5874  brtpos2  5897  tfrlemiex  5976  en1bg  6311  en1uniel  6315
 Copyright terms: Public domain W3C validator