Theorem uniexg 7730

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 4920	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2819	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7729	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3557	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  Vcvv 3475  ∪ cuni 4909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910

This theorem is referenced by:  uniex  7731  uniexd  7732  abnexg  7743  uniexb  7751  pwexr  7752  ssonuni  7767  ssonprc  7775  dmexg  7894  rnexg  7895  undefval  8261  onovuni  8342  tz7.44lem1  8405  tz7.44-3  8408  en1unielOLD  9029  disjen  9134  domss2  9136  fival  9407  fipwuni  9421  supexd  9448  cantnflem1  9684  dfac8clem  10027  onssnum  10035  dfac12lem1  10138  dfac12lem2  10139  fin1a2lem12  10406  hsmexlem1  10421  wrdexb  14475  restid  17379  prdsbas  17403  prdsplusg  17404  prdsmulr  17405  prdsvsca  17406  prdshom  17413  sscpwex  17762  pmtrfv  19320  istopon  22414  tgval  22458  eltg2  22461  tgss2  22490  neiptoptop  22635  restin  22670  restntr  22686  cnprest2  22794  pnrmopn  22847  cnrmnrm  22865  cmpsublem  22903  cmpsub  22904  cmpcld  22906  hausmapdom  23004  isref  23013  locfindis  23034  txbasex  23070  dfac14lem  23121  xkopt  23159  xkopjcn  23160  qtopval2  23200  elqtop  23201  fbssfi  23341  ptcmplem2  23557  cnextfval  23566  tuslem  23771  tuslemOLD  23772  madeval  27348  pliguhgr  29770  acunirnmpt2  31916  acunirnmpt2f  31917  ist0cld  32844  hasheuni  33114  insiga  33166  sigagenval  33169  omsval  33323  omssubadd  33330  sibfof  33370  sitmcl  33381  kur14  34238  cvmscld  34295  fobigcup  34903  hfuni  35187  isfne  35272  isfne4b  35274  fnemeet1  35299  tailfval  35305  bj-restuni2  36027  pibt2  36346  imaexALTV  37247  kelac2  41855  cnfex  43760  unidmex  43785  pwpwuni  43792  salgenval  45085  intsaluni  45093  salgenn0  45095  caragenunidm  45272  afv2ex  45970  iscnrm3rlem3  47623