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

Theorem unexg 6915
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 3198 . 2 (𝐴𝑉𝐴 ∈ V)
2 elex 3198 . 2 (𝐵𝑊𝐵 ∈ V)
3 unexb 6914 . . 3 ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴𝐵) ∈ V)
43biimpi 206 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐵) ∈ V)
51, 2, 4syl2an 494 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1987  Vcvv 3186  cun 3554
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4743  ax-nul 4751  ax-pr 4869  ax-un 6905
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-v 3188  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-sn 4151  df-pr 4153  df-uni 4405
This theorem is referenced by:  xpexg  6916  difex2  6921  difsnexi  6922  eldifpw  6926  ordunpr  6976  soex  7059  fnse  7242  suppun  7263  tposexg  7314  wfrlem15  7377  tfrlem12  7433  tfrlem16  7437  ralxpmap  7854  undifixp  7891  undom  7995  domunsncan  8007  domssex2  8067  domssex  8068  mapunen  8076  fsuppunbi  8243  elfiun  8283  brwdom2  8425  unwdomg  8436  alephprc  8869  cdadom3  8957  infunabs  8976  fin23lem11  9086  axdc2lem  9217  ttukeylem1  9278  fpwwe2lem13  9411  wunex2  9507  wuncval2  9516  hashunx  13118  hashf1lem1  13180  trclexlem  13670  trclun  13692  relexp0g  13699  relexpsucnnr  13702  isstruct2  15793  setsvalg  15811  setsid  15838  yonffth  16848  dmdprdsplit2  18369  basdif0  20671  fiuncmp  21120  refun0  21231  ptbasfi  21297  dfac14lem  21333  ptrescn  21355  xkoptsub  21370  filconn  21600  isufil2  21625  ufileu  21636  filufint  21637  fmfnfmlem4  21674  fmfnfm  21675  fclsfnflim  21744  flimfnfcls  21745  ptcmplem1  21769  elply2  23863  plyss  23866  wlkp1lem4  26449  resf1o  29360  locfinref  29702  esumsplit  29908  esumpad2  29911  sseqval  30243  bnj1149  30592  noextendltgt  31595  altxpexg  31748  hfun  31948  refssfne  32016  topjoin  32023  bj-2uplex  32678  ptrest  33061  poimirlem3  33065  paddval  34585  elrfi  36758  elmapresaun  36835  rclexi  37424  rtrclexlem  37425  trclubgNEW  37427  clcnvlem  37432  cnvrcl0  37434  dfrtrcl5  37438  iunrelexp0  37496  relexpmulg  37504  relexp01min  37507  relexpxpmin  37511  brtrclfv2  37521  sge0resplit  39946  sge0split  39949  setsv  40662  setrec1lem4  41746
  Copyright terms: Public domain W3C validator