MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unexg Structured version   Visualization version   GIF version

Theorem unexg 7688
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
StepHypRef Expression
1 elex 3466 . 2 (𝐴𝑉𝐴 ∈ V)
2 elex 3466 . 2 (𝐵𝑊𝐵 ∈ V)
3 unexb 7687 . . 3 ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴𝐵) ∈ V)
43biimpi 215 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐵) ∈ V)
51, 2, 4syl2an 597 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  Vcvv 3448  cun 3913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-sn 4592  df-pr 4594  df-uni 4871
This theorem is referenced by:  xpexg  7689  unexd  7693  difex2  7699  difsnexi  7700  eldifpw  7707  pwuncl  7709  ordunpr  7766  soex  7863  fnse  8070  suppun  8120  tposexg  8176  frrlem13  8234  wfrlem15OLD  8274  tfrlem12  8340  tfrlem16  8344  elmapresaun  8825  ralxpmap  8841  undifixp  8879  undom  9010  undomOLD  9011  domunsncan  9023  domssex2  9088  domssex  9089  mapunen  9097  sbthfilem  9152  fsuppunbi  9333  elfiun  9373  brwdom2  9516  unwdomg  9527  djuex  9851  djuexALT  9865  alephprc  10042  djudoml  10127  infunabs  10150  fin23lem11  10260  axdc2lem  10391  ttukeylem1  10452  fpwwe2lem12  10585  wunex2  10681  wuncval2  10690  hashunx  14293  hashf1lem1  14360  hashf1lem1OLD  14361  trclexlem  14886  trclun  14906  relexp0g  14914  relexpsucnnr  14917  isstruct2  17028  setsvalg  17045  setsid  17087  yonffth  18180  pwmndgplus  18752  dmdprdsplit2  19832  basdif0  22319  fiuncmp  22771  refun0  22882  ptbasfi  22948  dfac14lem  22984  ptrescn  23006  xkoptsub  23021  filconn  23250  isufil2  23275  ufileu  23286  filufint  23287  fmfnfmlem4  23324  fmfnfm  23325  fclsfnflim  23394  flimfnfcls  23395  ptcmplem1  23419  elply2  25573  plyss  25576  noeta2  27146  etasslt2  27175  scutbdaybnd2lim  27178  wlkp1lem4  28666  resf1o  31689  tocycfv  32000  tocycf  32008  locfinref  32462  esumsplit  32692  esumpad2  32695  sseqval  33028  bnj1149  33444  satfvsuc  33995  satf0suclem  34009  sat1el2xp  34013  fmlasuc0  34018  altxpexg  34592  hfun  34792  refssfne  34859  topjoin  34866  bj-2uplex  35522  ptrest  36106  poimirlem3  36110  paddval  38290  elrfi  41046  rtrclexlem  41962  clcnvlem  41969  cnvrcl0  41971  dfrtrcl5  41975  iunrelexp0  42048  relexpxpmin  42063  brtrclfv2  42073  sge0resplit  44721  sge0split  44724  setsv  45644  setrec1lem4  47209
  Copyright terms: Public domain W3C validator