Theorem uniexg 7775

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 4942	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2829	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7774	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3566	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  Vcvv 3488  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932

This theorem is referenced by:  uniex  7776  uniexd  7777  abnexg  7791  uniexb  7799  pwexr  7800  ssonuni  7815  ssonprc  7823  dmexg  7941  rnexg  7942  undefval  8317  onovuni  8398  tz7.44lem1  8461  tz7.44-3  8464  en1unielOLD  9094  disjen  9200  domss2  9202  fival  9481  fipwuni  9495  supexd  9522  cantnflem1  9758  dfac8clem  10101  onssnum  10109  dfac12lem1  10213  dfac12lem2  10214  fin1a2lem12  10480  hsmexlem1  10495  wrdexb  14573  restid  17493  prdsbas  17517  prdsplusg  17518  prdsmulr  17519  prdsvsca  17520  prdshom  17527  sscpwex  17876  pmtrfv  19494  istopon  22939  tgval  22983  eltg2  22986  tgss2  23015  neiptoptop  23160  restin  23195  restntr  23211  cnprest2  23319  pnrmopn  23372  cnrmnrm  23390  cmpsublem  23428  cmpsub  23429  cmpcld  23431  hausmapdom  23529  isref  23538  locfindis  23559  txbasex  23595  dfac14lem  23646  xkopt  23684  xkopjcn  23685  qtopval2  23725  elqtop  23726  fbssfi  23866  ptcmplem2  24082  cnextfval  24091  tuslem  24296  tuslemOLD  24297  madeval  27909  pliguhgr  30518  acunirnmpt2  32678  acunirnmpt2f  32679  ist0cld  33779  hasheuni  34049  insiga  34101  sigagenval  34104  omsval  34258  omssubadd  34265  sibfof  34305  sitmcl  34316  kur14  35184  cvmscld  35241  fobigcup  35864  hfuni  36148  isfne  36305  isfne4b  36307  fnemeet1  36332  tailfval  36338  bj-restuni2  37064  pibt2  37383  imaexALTV  38286  kelac2  43022  cnfex  44928  unidmex  44952  pwpwuni  44959  salgenval  46242  intsaluni  46250  salgenn0  46252  caragenunidm  46429  afv2ex  47129  iscnrm3rlem3  48622