Theorem uniexg 7181

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 4638	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2870	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7180	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3459	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1637   ∈ wcel 2156  Vcvv 3391  ∪ cuni 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-un 7175

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rex 3102  df-v 3393  df-uni 4631

This theorem is referenced by:  abnexg  7190  snnexOLD  7193  uniexb  7199  pwexr  7200  ssonuni  7212  ssonprc  7218  dmexg  7323  rnexg  7324  iunexg  7369  undefval  7633  onovuni  7671  tz7.44lem1  7733  tz7.44-3  7736  en1b  8256  en1uniel  8260  disjen  8352  domss2  8354  fival  8553  fipwuni  8567  supexd  8594  cantnflem1  8829  dfac8clem  9134  onssnum  9142  dfac12lem1  9246  dfac12lem2  9247  fin1a2lem12  9514  hsmexlem1  9529  axdc2lem  9551  ttukeylem3  9614  wrdexb  13523  restid  16295  prdsbas  16318  prdsplusg  16319  prdsmulr  16320  prdsvsca  16321  prdshom  16328  sscpwex  16675  pmtrfv  18069  frgpcyg  20125  istopon  20926  tgval  20969  eltg  20971  eltg2  20972  tgss2  21001  ntrval  21050  neiptoptop  21145  neiptopnei  21146  restin  21180  neitr  21194  restntr  21196  cnpresti  21302  cnprest  21303  cnprest2  21304  lmcnp  21318  pnrmopn  21357  cnrmnrm  21375  cmpsublem  21412  cmpsub  21413  cmpcld  21415  hausmapdom  21513  isref  21522  locfindis  21543  txbasex  21579  dfac14lem  21630  uptx  21638  xkopt  21668  xkopjcn  21669  qtopval2  21709  elqtop  21710  fbssfi  21850  ptcmplem2  22066  cnextfval  22075  cnextcn  22080  tuslem  22280  isppw  25050  pliguhgr  27665  elpwunicl  29692  acunirnmpt2  29783  acunirnmpt2f  29784  hasheuni  30468  insiga  30521  sigagenval  30524  braew  30626  omsval  30676  omssubaddlem  30682  omssubadd  30683  omsmeas  30706  sibfof  30723  sitmcl  30734  isrrvv  30826  rrvmulc  30836  bnj1489  31442  kur14  31516  cvmscld  31573  bdayimaon  32159  nosupno  32165  madeval  32251  fobigcup  32323  hfuni  32607  isfne  32650  isfne4b  32652  topjoin  32676  fnemeet1  32677  tailfval  32683  bj-restuni2  33357  mbfresfi  33763  supex2g  33839  kelac2  38130  cnfex  39675  unidmex  39704  pwpwuni  39712  uniexd  39768  unirnmap  39881  stoweidlem50  40740  stoweidlem57  40747  stoweidlem59  40749  stoweidlem60  40750  fourierdlem71  40867  salgenval  41014  intsaluni  41020  intsal  41021  salgenn0  41022  caragenval  41183  omecl  41193  caragenunidm  41198  afv2ex  41797  setrec1lem2  42997