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

Theorem unexg 7460
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 3513 . 2 (𝐴𝑉𝐴 ∈ V)
2 elex 3513 . 2 (𝐵𝑊𝐵 ∈ V)
3 unexb 7459 . . 3 ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴𝐵) ∈ V)
43biimpi 217 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐵) ∈ V)
51, 2, 4syl2an 595 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  Vcvv 3495  cun 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-sn 4560  df-pr 4562  df-uni 4833
This theorem is referenced by:  xpexg  7461  difex2  7470  difsnexi  7471  eldifpw  7478  pwuncl  7480  ordunpr  7529  soex  7614  fnse  7818  suppun  7841  tposexg  7897  wfrlem15  7960  tfrlem12  8016  tfrlem16  8020  elmapresaun  8434  ralxpmap  8449  undifixp  8487  undom  8594  domunsncan  8606  domssex2  8666  domssex  8667  mapunen  8675  fsuppunbi  8843  elfiun  8883  brwdom2  9026  unwdomg  9037  djuex  9326  djuexALT  9340  alephprc  9514  djudoml  9599  infunabs  9618  fin23lem11  9728  axdc2lem  9859  ttukeylem1  9920  fpwwe2lem13  10053  wunex2  10149  wuncval2  10158  hashunx  13737  hashf1lem1  13803  trclexlem  14344  trclun  14364  relexp0g  14371  relexpsucnnr  14374  isstruct2  16483  setsvalg  16502  setsid  16528  yonffth  17524  pwmndgplus  18040  dmdprdsplit2  19099  basdif0  21491  fiuncmp  21942  refun0  22053  ptbasfi  22119  dfac14lem  22155  ptrescn  22177  xkoptsub  22192  filconn  22421  isufil2  22446  ufileu  22457  filufint  22458  fmfnfmlem4  22495  fmfnfm  22496  fclsfnflim  22565  flimfnfcls  22566  ptcmplem1  22590  elply2  24715  plyss  24718  wlkp1lem4  27386  resf1o  30393  tocycfv  30679  tocycf  30687  locfinref  31005  esumsplit  31212  esumpad2  31215  sseqval  31546  bnj1149  31964  satfvsuc  32506  satf0suclem  32520  sat1el2xp  32524  fmlasuc0  32529  frrlem13  33033  ssltun1  33167  ssltun2  33168  altxpexg  33337  hfun  33537  refssfne  33604  topjoin  33611  bj-2uplex  34232  ptrest  34773  poimirlem3  34777  paddval  36816  elrfi  39171  rclexi  39855  rtrclexlem  39856  trclubgNEW  39858  clcnvlem  39863  cnvrcl0  39865  dfrtrcl5  39869  iunrelexp0  39927  relexpmulg  39935  relexp01min  39938  relexpxpmin  39942  brtrclfv2  39952  sge0resplit  42569  sge0split  42572  setsv  43419  setrec1lem4  44691
  Copyright terms: Public domain W3C validator