Theorem uniexg 7740

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 4882	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2847	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7739	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3521	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142  Vcvv 3454  ∪ cuni 4871

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-uni 4872

This theorem is used by:  uniex  7741  uniexd  7742  abnexg  7753  uniexb  7761  pwexr  7762  ssonuni  7777  ssonprc  7784  dmexg  7896  rnexg  7897  undefval  8271  onovuni  8327  tz7.44lem1  8390  tz7.44-3  8393  disjen  9120  domss2  9122  fival  9370  fipwuni  9384  supexd  9411  cantnflem1  9656  dfac8clem  10023  onssnum  10031  dfac12lem1  10134  dfac12lem2  10135  fin1a2lem12  10401  hsmexlem1  10416  wrdexb  14569  restid  17492  prdsbas  17516  prdsplusg  17517  prdsmulr  17518  prdsvsca  17519  prdshom  17526  sscpwex  17878  pmtrfv  19528  istopon  23080  tgval  23123  eltg2  23126  tgss2  23155  neiptoptop  23299  restin  23334  restntr  23350  cnprest2  23458  pnrmopn  23511  cnrmnrm  23529  cmpsublem  23567  cmpsub  23568  cmpcld  23570  hausmapdom  23668  isref  23677  locfindis  23698  txbasex  23734  dfac14lem  23785  xkopt  23823  xkopjcn  23824  qtopval2  23864  elqtop  23865  fbssfi  24005  ptcmplem2  24221  cnextfval  24230  tuslem  24434  madeval  28036  pliguhgr  30849  acunirnmpt2  33016  acunirnmpt2f  33017  ist0cld  34232  hasheuni  34484  insiga  34536  sigagenval  34539  omsval  34692  omssubadd  34699  sibfof  34739  sitmcl  34750  kur14  35716  cvmscld  35773  fobigcup  36398  hfuni  36684  isfne  36878  isfne4b  36880  fnemeet1  36905  tailfval  36911  bj-restuni2  37768  pibt2  38091  kelac2  43820  cnfex  45776  unidmex  45798  pwpwuni  45805  salgenval  47063  intsaluni  47071  salgenn0  47073  caragenunidm  47250  afv2ex  47979  iscnrm3rlem3  49748