Theorem uniexg 7571

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 4847	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2823	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7570	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3495	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  Vcvv 3422  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837

This theorem is referenced by:  uniex  7572  uniexd  7573  abnexg  7584  uniexb  7592  pwexr  7593  ssonuni  7607  ssonprc  7614  dmexg  7724  rnexg  7725  undefval  8063  onovuni  8144  tz7.44lem1  8207  tz7.44-3  8210  en1unielOLD  8773  disjen  8870  domss2  8872  fival  9101  fipwuni  9115  supexd  9142  cantnflem1  9377  dfac8clem  9719  onssnum  9727  dfac12lem1  9830  dfac12lem2  9831  fin1a2lem12  10098  hsmexlem1  10113  wrdexb  14156  restid  17061  prdsbas  17085  prdsplusg  17086  prdsmulr  17087  prdsvsca  17088  prdshom  17095  sscpwex  17444  pmtrfv  18975  istopon  21969  tgval  22013  eltg2  22016  tgss2  22045  neiptoptop  22190  restin  22225  restntr  22241  cnprest2  22349  pnrmopn  22402  cnrmnrm  22420  cmpsublem  22458  cmpsub  22459  cmpcld  22461  hausmapdom  22559  isref  22568  locfindis  22589  txbasex  22625  dfac14lem  22676  xkopt  22714  xkopjcn  22715  qtopval2  22755  elqtop  22756  fbssfi  22896  ptcmplem2  23112  cnextfval  23121  tuslem  23326  tuslemOLD  23327  pliguhgr  28749  acunirnmpt2  30899  acunirnmpt2f  30900  ist0cld  31685  hasheuni  31953  insiga  32005  sigagenval  32008  omsval  32160  omssubadd  32167  sibfof  32207  sitmcl  32218  kur14  33078  cvmscld  33135  madeval  33963  fobigcup  34129  hfuni  34413  isfne  34455  isfne4b  34457  fnemeet1  34482  tailfval  34488  bj-restuni2  35196  pibt2  35515  imaexALTV  36392  kelac2  40806  cnfex  42460  unidmex  42487  pwpwuni  42494  salgenval  43752  intsaluni  43758  salgenn0  43760  caragenunidm  43936  afv2ex  44593  iscnrm3rlem3  46124