Theorem uniexg 7120

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 4596	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2824	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7119	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3406	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1632   ∈ wcel 2139  Vcvv 3340  ∪ cuni 4588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-un 7114

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-v 3342  df-uni 4589

This theorem is referenced by:  abnexg  7129  snnexOLD  7132  uniexb  7138  pwexr  7139  ssonuni  7151  ssonprc  7157  dmexg  7262  rnexg  7263  iunexg  7308  undefval  7571  onovuni  7608  tz7.44lem1  7670  tz7.44-3  7673  en1b  8189  en1uniel  8193  disjen  8282  domss2  8284  fival  8483  fipwuni  8497  supexd  8524  cantnflem1  8759  dfac8clem  9045  onssnum  9053  dfac12lem1  9157  dfac12lem2  9158  fin1a2lem12  9425  hsmexlem1  9440  axdc2lem  9462  ttukeylem3  9525  wrdexb  13502  restid  16296  prdsbas  16319  prdsplusg  16320  prdsmulr  16321  prdsvsca  16322  prdshom  16329  sscpwex  16676  pmtrfv  18072  frgpcyg  20124  istopon  20919  tgval  20961  eltg  20963  eltg2  20964  tgss2  20993  ntrval  21042  neiptoptop  21137  neiptopnei  21138  restin  21172  neitr  21186  restntr  21188  cnpresti  21294  cnprest  21295  cnprest2  21296  lmcnp  21310  pnrmopn  21349  cnrmnrm  21367  cmpsublem  21404  cmpsub  21405  cmpcld  21407  hausmapdom  21505  isref  21514  locfindis  21535  txbasex  21571  dfac14lem  21622  uptx  21630  xkopt  21660  xkopjcn  21661  qtopval2  21701  elqtop  21702  fbssfi  21842  ptcmplem2  22058  cnextfval  22067  cnextcn  22072  tuslem  22272  isppw  25039  pliguhgr  27649  elpwunicl  29678  acunirnmpt2  29769  acunirnmpt2f  29770  hasheuni  30456  insiga  30509  sigagenval  30512  braew  30614  omsval  30664  omssubaddlem  30670  omssubadd  30671  omsmeas  30694  sibfof  30711  sitmcl  30722  isrrvv  30814  rrvmulc  30824  bnj1489  31431  kur14  31505  cvmscld  31562  bdayimaon  32149  nosupno  32155  madeval  32241  fobigcup  32313  hfuni  32597  isfne  32640  isfne4b  32642  topjoin  32666  fnemeet1  32667  tailfval  32673  bj-restuni2  33357  mbfresfi  33769  supex2g  33845  kelac2  38137  cnfex  39686  unidmex  39716  pwpwuni  39724  uniexd  39780  unirnmap  39899  stoweidlem50  40770  stoweidlem57  40777  stoweidlem59  40779  stoweidlem60  40780  fourierdlem71  40897  salgenval  41044  intsaluni  41050  intsal  41051  salgenn0  41052  caragenval  41213  omecl  41223  caragenunidm  41228  setrec1lem2  42945