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

Theorem unexg 7461
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 3510 . 2 (𝐴𝑉𝐴 ∈ V)
2 elex 3510 . 2 (𝐵𝑊𝐵 ∈ V)
3 unexb 7460 . . 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 3492  cun 3931
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 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320  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 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-sn 4558  df-pr 4560  df-uni 4831
This theorem is referenced by:  xpexg  7462  difex2  7471  difsnexi  7472  eldifpw  7479  pwuncl  7481  ordunpr  7530  soex  7615  fnse  7816  suppun  7839  tposexg  7895  wfrlem15  7958  tfrlem12  8014  tfrlem16  8018  elmapresaun  8433  ralxpmap  8448  undifixp  8486  undom  8593  domunsncan  8605  domssex2  8665  domssex  8666  mapunen  8674  fsuppunbi  8842  elfiun  8882  brwdom2  9025  unwdomg  9036  djuex  9325  djuexALT  9339  alephprc  9513  djudoml  9598  infunabs  9617  fin23lem11  9727  axdc2lem  9858  ttukeylem1  9919  fpwwe2lem13  10052  wunex2  10148  wuncval2  10157  hashunx  13735  hashf1lem1  13801  trclexlem  14342  trclun  14362  relexp0g  14369  relexpsucnnr  14372  isstruct2  16481  setsvalg  16500  setsid  16526  yonffth  17522  pwmndgplus  18038  dmdprdsplit2  19097  basdif0  21489  fiuncmp  21940  refun0  22051  ptbasfi  22117  dfac14lem  22153  ptrescn  22175  xkoptsub  22190  filconn  22419  isufil2  22444  ufileu  22455  filufint  22456  fmfnfmlem4  22493  fmfnfm  22494  fclsfnflim  22563  flimfnfcls  22564  ptcmplem1  22588  elply2  24713  plyss  24716  wlkp1lem4  27385  resf1o  30392  tocycfv  30678  tocycf  30686  locfinref  31004  esumsplit  31211  esumpad2  31214  sseqval  31545  bnj1149  31963  satfvsuc  32505  satf0suclem  32519  sat1el2xp  32523  fmlasuc0  32528  frrlem13  33032  ssltun1  33166  ssltun2  33167  altxpexg  33336  hfun  33536  refssfne  33603  topjoin  33610  bj-2uplex  34231  ptrest  34772  poimirlem3  34776  paddval  36814  elrfi  39169  rclexi  39853  rtrclexlem  39854  trclubgNEW  39856  clcnvlem  39861  cnvrcl0  39863  dfrtrcl5  39867  iunrelexp0  39925  relexpmulg  39933  relexp01min  39936  relexpxpmin  39940  brtrclfv2  39950  sge0resplit  42565  sge0split  42568  setsv  43415  setrec1lem4  44721
  Copyright terms: Public domain W3C validator