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

Theorem unexg 7456
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 3462 . 2 (𝐴𝑉𝐴 ∈ V)
2 elex 3462 . 2 (𝐵𝑊𝐵 ∈ V)
3 unexb 7455 . . 3 ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴𝐵) ∈ V)
43biimpi 219 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐵) ∈ V)
51, 2, 4syl2an 598 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2112  Vcvv 3444  cun 3882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-rab 3118  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-sn 4529  df-pr 4531  df-uni 4804
This theorem is referenced by:  xpexg  7457  difex2  7466  difsnexi  7467  eldifpw  7474  pwuncl  7476  ordunpr  7525  soex  7612  fnse  7814  suppun  7837  tposexg  7893  wfrlem15  7956  tfrlem12  8012  tfrlem16  8016  elmapresaun  8431  ralxpmap  8447  undifixp  8485  undom  8592  domunsncan  8604  domssex2  8665  domssex  8666  mapunen  8674  fsuppunbi  8842  elfiun  8882  brwdom2  9025  unwdomg  9036  djuex  9325  djuexALT  9339  alephprc  9514  djudoml  9599  infunabs  9622  fin23lem11  9732  axdc2lem  9863  ttukeylem1  9924  fpwwe2lem13  10057  wunex2  10153  wuncval2  10162  hashunx  13747  hashf1lem1  13813  trclexlem  14349  trclun  14369  relexp0g  14376  relexpsucnnr  14379  isstruct2  16488  setsvalg  16507  setsid  16533  yonffth  17529  pwmndgplus  18095  dmdprdsplit2  19164  basdif0  21561  fiuncmp  22012  refun0  22123  ptbasfi  22189  dfac14lem  22225  ptrescn  22247  xkoptsub  22262  filconn  22491  isufil2  22516  ufileu  22527  filufint  22528  fmfnfmlem4  22565  fmfnfm  22566  fclsfnflim  22635  flimfnfcls  22636  ptcmplem1  22660  elply2  24796  plyss  24799  wlkp1lem4  27469  resf1o  30495  tocycfv  30804  tocycf  30812  locfinref  31194  esumsplit  31420  esumpad2  31423  sseqval  31754  bnj1149  32172  satfvsuc  32716  satf0suclem  32730  sat1el2xp  32734  fmlasuc0  32739  frrlem13  33243  ssltun1  33377  ssltun2  33378  altxpexg  33547  hfun  33747  refssfne  33814  topjoin  33821  bj-2uplex  34453  ptrest  35049  poimirlem3  35053  paddval  37087  unexd  39392  elrfi  39622  rclexi  40302  rtrclexlem  40303  trclubgNEW  40305  clcnvlem  40310  cnvrcl0  40312  dfrtrcl5  40316  iunrelexp0  40390  relexpmulg  40398  relexp01min  40401  relexpxpmin  40405  brtrclfv2  40415  sge0resplit  43032  sge0split  43035  setsv  43882  setrec1lem4  45207
  Copyright terms: Public domain W3C validator