Theorem uniexg 7469

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 4852	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2900	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7468	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3570	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2113  Vcvv 3497  ∪ cuni 4841

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-in 3946  df-ss 3955  df-uni 4842

This theorem is referenced by:  uniex  7470  uniexd  7471  abnexg  7481  uniexb  7489  pwexr  7490  ssonuni  7504  ssonprc  7510  dmexg  7616  rnexg  7617  undefval  7945  onovuni  7982  tz7.44lem1  8044  tz7.44-3  8047  en1uniel  8584  disjen  8677  domss2  8679  fival  8879  fipwuni  8893  supexd  8920  cantnflem1  9155  dfac8clem  9461  onssnum  9469  dfac12lem1  9572  dfac12lem2  9573  fin1a2lem12  9836  hsmexlem1  9851  wrdexb  13876  restid  16710  prdsbas  16733  prdsplusg  16734  prdsmulr  16735  prdsvsca  16736  prdshom  16743  sscpwex  17088  pmtrfv  18583  istopon  21523  tgval  21566  eltg2  21569  tgss2  21598  neiptoptop  21742  restin  21777  restntr  21793  cnprest2  21901  pnrmopn  21954  cnrmnrm  21972  cmpsublem  22010  cmpsub  22011  cmpcld  22013  hausmapdom  22111  isref  22120  locfindis  22141  txbasex  22177  dfac14lem  22228  xkopt  22266  xkopjcn  22267  qtopval2  22307  elqtop  22308  fbssfi  22448  ptcmplem2  22664  cnextfval  22673  tuslem  22879  pliguhgr  28266  acunirnmpt2  30408  acunirnmpt2f  30409  hasheuni  31348  insiga  31400  sigagenval  31403  omsval  31555  omssubadd  31562  sibfof  31602  sitmcl  31613  kur14  32467  cvmscld  32524  madeval  33293  fobigcup  33365  hfuni  33649  isfne  33691  isfne4b  33693  fnemeet1  33718  tailfval  33724  bj-restuni2  34393  pibt2  34702  imaexALTV  35591  kelac2  39671  cnfex  41291  unidmex  41318  pwpwuni  41325  salgenval  42613  intsaluni  42619  salgenn0  42621  caragenunidm  42797  afv2ex  43420