Theorem uniexg 7778

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  Vcvv 3454  ∪ cuni 4870

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-un 7772

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4871

This theorem is used by:  uniex  7779  uniexd  7780  abnexg  7791  uniexb  7799  pwexr  7800  ssonuni  7815  ssonprc  7822  dmexg  7934  rnexg  7935  undefval  8319  onovuni  8375  tz7.44lem1  8438  tz7.44-3  8441  disjen  9178  domss2  9180  fival  9428  fipwuni  9442  supexd  9469  cantnflem1  9714  hfuniOLD  9949  dfac8clem  10135  onssnum  10143  dfac12lem1  10246  dfac12lem2  10247  fin1a2lem12  10513  hsmexlem1  10528  wrdexb  14694  restid  17630  prdsbas  17654  prdsplusg  17655  prdsmulr  17656  prdsvsca  17657  prdshom  17664  sscpwex  18016  pmtrfv  19693  istopon  23257  tgval  23300  eltg2  23303  tgss2  23332  neiptoptop  23476  restin  23511  restntr  23527  cnprest2  23635  pnrmopn  23688  cnrmnrm  23706  cmpsublem  23744  cmpsub  23745  cmpcld  23747  hausmapdom  23846  isref  23855  locfindis  23876  txbasex  23912  dfac14lem  23963  xkopt  24001  xkopjcn  24002  qtopval2  24042  elqtop  24043  fbssfi  24183  ptcmplem2  24399  cnextfval  24408  tuslem  24612  madeval  28245  pliguhgr  31115  acunirnmpt2  33323  acunirnmpt2f  33324  ist0cld  34532  reff  34538  hasheuni  34784  insiga  34837  sigagenval  34840  omsval  34992  omssubadd  34999  sibfof  35039  sitmcl  35050  kur14  36147  cvmscld  36204  cardprcr  36632  fobigcup  36839  isfne  37304  isfne4b  37306  fnemeet1  37331  tailfval  37337  bj-restuni2  38209  kelac2  44258  cnfex  46248  unidmex  46270  pwpwuni  46277  salgenval  47534  intsaluni  47542  salgenn0  47544  caragenunidm  47721  afv2ex  48487  iscnrm3rlem3  50259