Theorem unexg 7512

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 3416	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		elex 3416	. 2 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
3		unexb 7511	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V)
4	3	biimpi 219	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V)
5	1, 2, 4	syl2an 599	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2112  Vcvv 3398   ∪ cun 3851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-sn 4528  df-pr 4530  df-uni 4806

This theorem is referenced by:  xpexg  7513  unexd  7517  difex2  7523  difsnexi  7524  eldifpw  7531  pwuncl  7533  ordunpr  7583  soex  7677  fnse  7878  suppun  7904  tposexg  7960  frrlem13  8017  wfrlem15  8047  tfrlem12  8103  tfrlem16  8107  elmapresaun  8539  ralxpmap  8555  undifixp  8593  undom  8711  domunsncan  8723  domssex2  8784  domssex  8785  mapunen  8793  fsuppunbi  8984  elfiun  9024  brwdom2  9167  unwdomg  9178  djuex  9489  djuexALT  9503  alephprc  9678  djudoml  9763  infunabs  9786  fin23lem11  9896  axdc2lem  10027  ttukeylem1  10088  fpwwe2lem12  10221  wunex2  10317  wuncval2  10326  hashunx  13918  hashf1lem1  13985  hashf1lem1OLD  13986  trclexlem  14522  trclun  14542  relexp0g  14550  relexpsucnnr  14553  isstruct2  16676  setsvalg  16694  setsid  16719  yonffth  17746  pwmndgplus  18316  dmdprdsplit2  19387  basdif0  21804  fiuncmp  22255  refun0  22366  ptbasfi  22432  dfac14lem  22468  ptrescn  22490  xkoptsub  22505  filconn  22734  isufil2  22759  ufileu  22770  filufint  22771  fmfnfmlem4  22808  fmfnfm  22809  fclsfnflim  22878  flimfnfcls  22879  ptcmplem1  22903  elply2  25044  plyss  25047  wlkp1lem4  27718  resf1o  30739  tocycfv  31049  tocycf  31057  locfinref  31459  esumsplit  31687  esumpad2  31690  sseqval  32021  bnj1149  32439  satfvsuc  32990  satf0suclem  33004  sat1el2xp  33008  fmlasuc0  33013  noeta2  33665  etasslt2  33694  scutbdaybnd2lim  33697  altxpexg  33966  hfun  34166  refssfne  34233  topjoin  34240  bj-2uplex  34898  ptrest  35462  poimirlem3  35466  paddval  37498  elrfi  40160  rclexi  40840  rtrclexlem  40841  trclubgNEW  40843  clcnvlem  40848  cnvrcl0  40850  dfrtrcl5  40854  iunrelexp0  40928  relexpmulg  40936  relexp01min  40939  relexpxpmin  40943  brtrclfv2  40953  sge0resplit  43562  sge0split  43565  setsv  44446  setrec1lem4  46010