Theorem uniexg 6908

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 4410	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2683	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 6907	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3252	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1480   ∈ wcel 1987  Vcvv 3186  ∪ cuni 4402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-un 6902

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-v 3188  df-uni 4403

This theorem is referenced by:  snnex  6917  uniexb  6921  ssonuni  6933  ssonprc  6939  dmexg  7044  rnexg  7045  iunexg  7089  undefval  7347  onovuni  7384  tz7.44lem1  7446  tz7.44-3  7449  en1b  7968  en1uniel  7972  disjen  8061  domss2  8063  fival  8262  fipwuni  8276  supexd  8303  cantnflem1  8530  dfac8clem  8799  onssnum  8807  dfac12lem1  8909  dfac12lem2  8910  fin1a2lem12  9177  hsmexlem1  9192  axdc2lem  9214  ttukeylem3  9277  wrdexb  13255  restid  16015  prdsbas  16038  prdsplusg  16039  prdsmulr  16040  prdsvsca  16041  prdshom  16048  sscpwex  16396  pmtrfv  17793  frgpcyg  19841  istopon  20640  tgval  20670  eltg  20672  eltg2  20673  tgss2  20702  ntrval  20750  neiptoptop  20845  neiptopnei  20846  restin  20880  neitr  20894  restntr  20896  cnpresti  21002  cnprest  21003  cnprest2  21004  lmcnp  21018  pnrmopn  21057  cnrmnrm  21075  cmpsublem  21112  cmpsub  21113  cmpcld  21115  hausmapdom  21213  isref  21222  locfindis  21243  txbasex  21279  dfac14lem  21330  uptx  21338  xkopt  21368  xkopjcn  21369  qtopval2  21409  elqtop  21410  fbssfi  21551  ptcmplem2  21767  cnextfval  21776  cnextcn  21781  tuslem  21981  isppw  24740  pliguhgr  27187  elpwunicl  29217  acunirnmpt2  29302  acunirnmpt2f  29303  hasheuni  29928  insiga  29981  sigagenval  29984  braew  30086  omsval  30136  omssubaddlem  30142  omssubadd  30143  omsmeas  30166  sibfof  30183  sitmcl  30194  isrrvv  30286  rrvmulc  30296  bnj1489  30832  kur14  30906  cvmscld  30963  nobndlem1  31555  nosino  31575  fobigcup  31649  hfuni  31933  isfne  31976  isfne4b  31978  topjoin  32002  fnemeet1  32003  tailfval  32009  bj-restuni2  32688  bj-xnex  32701  mbfresfi  33088  supex2g  33164  kelac2  37115  cnfex  38670  unidmex  38702  pwpwuni  38710  uniexd  38766  unirnmap  38874  stoweidlem50  39574  stoweidlem57  39581  stoweidlem59  39583  stoweidlem60  39584  fourierdlem71  39701  salgenval  39848  intsaluni  39854  intsal  39855  salgenn0  39856  caragenval  40014  omecl  40024  caragenunidm  40029  setrec1lem2  41728