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

Theorem unexg 7124
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 3352 . 2 (𝐴𝑉𝐴 ∈ V)
2 elex 3352 . 2 (𝐵𝑊𝐵 ∈ V)
3 unexb 7123 . . 3 ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴𝐵) ∈ V)
43biimpi 206 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐵) ∈ V)
51, 2, 4syl2an 495 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2139  Vcvv 3340  cun 3713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-sn 4322  df-pr 4324  df-uni 4589
This theorem is referenced by:  xpexg  7125  difex2  7134  difsnexi  7135  eldifpw  7141  ordunpr  7191  soex  7274  fnse  7462  suppun  7483  tposexg  7535  wfrlem15  7598  tfrlem12  7654  tfrlem16  7658  ralxpmap  8073  undifixp  8110  undom  8213  domunsncan  8225  domssex2  8285  domssex  8286  mapunen  8294  fsuppunbi  8461  elfiun  8501  brwdom2  8643  unwdomg  8654  alephprc  9112  cdadom3  9202  infunabs  9221  fin23lem11  9331  axdc2lem  9462  ttukeylem1  9523  fpwwe2lem13  9656  wunex2  9752  wuncval2  9761  hashunx  13367  hashf1lem1  13431  trclexlem  13934  trclun  13954  relexp0g  13961  relexpsucnnr  13964  isstruct2  16069  setsvalg  16089  setsid  16116  yonffth  17125  dmdprdsplit2  18645  basdif0  20959  fiuncmp  21409  refun0  21520  ptbasfi  21586  dfac14lem  21622  ptrescn  21644  xkoptsub  21659  filconn  21888  isufil2  21913  ufileu  21924  filufint  21925  fmfnfmlem4  21962  fmfnfm  21963  fclsfnflim  22032  flimfnfcls  22033  ptcmplem1  22057  elply2  24151  plyss  24154  wlkp1lem4  26783  resf1o  29814  locfinref  30217  esumsplit  30424  esumpad2  30427  sseqval  30759  bnj1149  31170  ssltun1  32221  ssltun2  32222  altxpexg  32391  hfun  32591  refssfne  32659  topjoin  32666  bj-2uplex  33316  cnfinltrel  33552  ptrest  33721  poimirlem3  33725  paddval  35587  elrfi  37759  elmapresaun  37836  rclexi  38424  rtrclexlem  38425  trclubgNEW  38427  clcnvlem  38432  cnvrcl0  38434  dfrtrcl5  38438  iunrelexp0  38496  relexpmulg  38504  relexp01min  38507  relexpxpmin  38511  brtrclfv2  38521  sge0resplit  41126  sge0split  41129  setsv  41858  setrec1lem4  42947
  Copyright terms: Public domain W3C validator