Theorem unexg 7735

Description: A union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.)

Assertion

Ref	Expression
unexg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)

Proof of Theorem unexg

Step	Hyp	Ref	Expression
1		elex 3492	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		elex 3492	. 2 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
3		unexb 7734	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V)
4	3	biimpi 215	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V)
5	1, 2, 4	syl2an 596	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Vcvv 3474   ∪ cun 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7724

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-sn 4629  df-pr 4631  df-uni 4909

This theorem is referenced by:  xpexg  7736  unexd  7740  difex2  7746  difsnexi  7747  eldifpw  7754  pwuncl  7756  ordunpr  7813  soex  7911  fnse  8118  suppun  8168  tposexg  8224  frrlem13  8282  wfrlem15OLD  8322  tfrlem12  8388  tfrlem16  8392  elmapresaun  8873  ralxpmap  8889  undifixp  8927  undom  9058  undomOLD  9059  domunsncan  9071  domssex2  9136  domssex  9137  mapunen  9145  sbthfilem  9200  fsuppunbi  9383  elfiun  9424  brwdom2  9567  unwdomg  9578  djuex  9902  djuexALT  9916  alephprc  10093  djudoml  10178  infunabs  10201  fin23lem11  10311  axdc2lem  10442  ttukeylem1  10503  fpwwe2lem12  10636  wunex2  10732  wuncval2  10741  hashunx  14345  hashf1lem1  14414  hashf1lem1OLD  14415  trclexlem  14940  trclun  14960  relexp0g  14968  relexpsucnnr  14971  isstruct2  17081  setsvalg  17098  setsid  17140  yonffth  18236  pwmndgplus  18815  dmdprdsplit2  19915  basdif0  22455  fiuncmp  22907  refun0  23018  ptbasfi  23084  dfac14lem  23120  ptrescn  23142  xkoptsub  23157  filconn  23386  isufil2  23411  ufileu  23422  filufint  23423  fmfnfmlem4  23460  fmfnfm  23461  fclsfnflim  23530  flimfnfcls  23531  ptcmplem1  23555  elply2  25709  plyss  25712  noeta2  27283  etasslt2  27312  scutbdaybnd2lim  27315  wlkp1lem4  28930  resf1o  31950  tocycfv  32263  tocycf  32271  locfinref  32816  esumsplit  33046  esumpad2  33049  sseqval  33382  bnj1149  33798  satfvsuc  34347  satf0suclem  34361  sat1el2xp  34365  fmlasuc0  34370  altxpexg  34945  hfun  35145  refssfne  35238  topjoin  35245  bj-2uplex  35898  ptrest  36482  poimirlem3  36486  paddval  38664  evlselvlem  41160  elrfi  41422  rtrclexlem  42357  clcnvlem  42364  cnvrcl0  42366  dfrtrcl5  42370  iunrelexp0  42443  relexpxpmin  42458  brtrclfv2  42468  sge0resplit  45112  sge0split  45115  setsv  46036  setrec1lem4  47725