Theorem uniexg 7696

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.

Step	Hyp	Ref	Expression
1		unieq 4878	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2813	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7695	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3517	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3444  ∪ cuni 4867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-uni 4868

This theorem is referenced by:  uniex  7697  uniexd  7698  abnexg  7712  uniexb  7720  pwexr  7721  ssonuni  7736  ssonprc  7743  dmexg  7857  rnexg  7858  undefval  8232  onovuni  8288  tz7.44lem1  8350  tz7.44-3  8353  disjen  9075  domss2  9077  fival  9339  fipwuni  9353  supexd  9380  cantnflem1  9620  dfac8clem  9963  onssnum  9971  dfac12lem1  10075  dfac12lem2  10076  fin1a2lem12  10342  hsmexlem1  10357  wrdexb  14468  restid  17373  prdsbas  17397  prdsplusg  17398  prdsmulr  17399  prdsvsca  17400  prdshom  17407  sscpwex  17758  pmtrfv  19367  istopon  22833  tgval  22876  eltg2  22879  tgss2  22908  neiptoptop  23052  restin  23087  restntr  23103  cnprest2  23211  pnrmopn  23264  cnrmnrm  23282  cmpsublem  23320  cmpsub  23321  cmpcld  23323  hausmapdom  23421  isref  23430  locfindis  23451  txbasex  23487  dfac14lem  23538  xkopt  23576  xkopjcn  23577  qtopval2  23617  elqtop  23618  fbssfi  23758  ptcmplem2  23974  cnextfval  23983  tuslem  24188  madeval  27798  pliguhgr  30466  acunirnmpt2  32635  acunirnmpt2f  32636  ist0cld  33817  hasheuni  34069  insiga  34121  sigagenval  34124  omsval  34278  omssubadd  34285  sibfof  34325  sitmcl  34336  kur14  35197  cvmscld  35254  fobigcup  35882  hfuni  36166  isfne  36321  isfne4b  36323  fnemeet1  36348  tailfval  36354  bj-restuni2  37080  pibt2  37399  kelac2  43048  cnfex  45016  unidmex  45038  pwpwuni  45045  salgenval  46313  intsaluni  46321  salgenn0  46323  caragenunidm  46500  afv2ex  47209  iscnrm3rlem3  48924