Theorem uniexg 4486

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 3859	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2274	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vex 2775	. . 3 ⊢ 𝑥 ∈ V
4	3	uniex 4484	. 2 ⊢ ∪ 𝑥 ∈ V
5	2, 4	vtoclg 2833	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2176  Vcvv 2772  ∪ cuni 3850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-13 2178  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-un 4480

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-uni 3851

This theorem is referenced by:  uniexd  4487  abnexg  4493  snnex  4495  uniexb  4520  ssonuni  4536  dmexg  4942  rnexg  4943  elxp4  5170  elxp5  5171  iotaexab  5250  relrnfvex  5594  fvexg  5595  sefvex  5597  riotaexg  5903  iunexg  6204  1stvalg  6228  2ndvalg  6229  cnvf1o  6311  brtpos2  6337  tfrlemiex  6417  tfr1onlemex  6433  tfrcllemex  6446  en1bg  6892  en1uniel  6896  fival  7072  suplocexprlem2b  7827  suplocexprlemlub  7837  wrdexb  11006  restid  13082  tgval  13094  tgvalex  13095  istopon  14485  eltg  14524  eltg2  14525  tgss2  14551  ntrval  14582  restin  14648  cnovex  14668  cnprcl2k  14678  cnptopresti  14710  cnptoprest  14711  cnptoprest2  14712  lmtopcnp  14722  txbasex  14729  uptx  14746  reldvg  15151