Theorem uniexg 7718

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 4884	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2814	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7717	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3523	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3450  ∪ cuni 4873

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 2702  ax-sep 5253  ax-un 7713

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3933  df-uni 4874

This theorem is referenced by:  uniex  7719  uniexd  7720  abnexg  7734  uniexb  7742  pwexr  7743  ssonuni  7758  ssonprc  7765  dmexg  7879  rnexg  7880  undefval  8257  onovuni  8313  tz7.44lem1  8375  tz7.44-3  8378  disjen  9103  domss2  9105  fival  9369  fipwuni  9383  supexd  9410  cantnflem1  9648  dfac8clem  9991  onssnum  9999  dfac12lem1  10103  dfac12lem2  10104  fin1a2lem12  10370  hsmexlem1  10385  wrdexb  14496  restid  17402  prdsbas  17426  prdsplusg  17427  prdsmulr  17428  prdsvsca  17429  prdshom  17436  sscpwex  17783  pmtrfv  19388  istopon  22805  tgval  22848  eltg2  22851  tgss2  22880  neiptoptop  23024  restin  23059  restntr  23075  cnprest2  23183  pnrmopn  23236  cnrmnrm  23254  cmpsublem  23292  cmpsub  23293  cmpcld  23295  hausmapdom  23393  isref  23402  locfindis  23423  txbasex  23459  dfac14lem  23510  xkopt  23548  xkopjcn  23549  qtopval2  23589  elqtop  23590  fbssfi  23730  ptcmplem2  23946  cnextfval  23955  tuslem  24160  madeval  27766  pliguhgr  30421  acunirnmpt2  32590  acunirnmpt2f  32591  ist0cld  33829  hasheuni  34081  insiga  34133  sigagenval  34136  omsval  34290  omssubadd  34297  sibfof  34337  sitmcl  34348  kur14  35203  cvmscld  35260  fobigcup  35883  hfuni  36167  isfne  36322  isfne4b  36324  fnemeet1  36349  tailfval  36355  bj-restuni2  37081  pibt2  37400  kelac2  43047  cnfex  45015  unidmex  45037  pwpwuni  45044  salgenval  46312  intsaluni  46320  salgenn0  46322  caragenunidm  46499  afv2ex  47205  iscnrm3rlem3  48920