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

Theorem unex 7685
Description: The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.)
Hypotheses
Ref Expression
unex.1 𝐴 ∈ V
unex.2 𝐵 ∈ V
Assertion
Ref Expression
unex (𝐴𝐵) ∈ V

Proof of Theorem unex
StepHypRef Expression
1 unex.1 . . 3 𝐴 ∈ V
2 unex.2 . . 3 𝐵 ∈ V
31, 2unipr 4888 . 2 {𝐴, 𝐵} = (𝐴𝐵)
4 prex 5394 . . 3 {𝐴, 𝐵} ∈ V
54uniex 7683 . 2 {𝐴, 𝐵} ∈ V
63, 5eqeltrri 2835 1 (𝐴𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3448  cun 3913  {cpr 4593   cuni 4870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-sn 4592  df-pr 4594  df-uni 4871
This theorem is referenced by:  tpex  7686  unexb  7687  fvclex  7896  naddcllem  8627  ralxpmap  8841  unen  8997  undom  9010  enfixsn  9032  sbthlem10  9043  dif1en  9111  dif1enOLD  9113  findcard2  9115  pwfilem  9128  unxpdomlem3  9203  isinf  9211  isinfOLD  9212  findcard2OLD  9235  ac6sfi  9238  pwfilemOLD  9297  cnfcomlem  9642  trcl  9671  tc2  9685  rankxpu  9819  rankxplim  9822  rankxplim3  9824  r0weon  9955  infxpenlem  9956  dfac4  10065  dfac2b  10073  kmlem2  10094  cfsmolem  10213  isfin1-3  10329  axdc2lem  10391  axdc3lem4  10396  axcclem  10400  ttukeylem3  10454  gchac  10624  wunex2  10681  wuncval2  10690  inar1  10718  nn0ex  12426  xrex  12919  seqexw  13929  hashbclem  14356  incexclem  15728  ramub1lem2  16906  prdsval  17344  imasval  17400  ipoval  18426  plusffval  18510  smndex1bas  18723  smndex1sgrp  18725  smndex1mnd  18727  smndex1id  18728  grpinvfval  18796  grpsubfval  18801  mulgfval  18881  staffval  20322  scaffval  20356  lpival  20731  xrsex  20828  ipffval  21068  islindf4  21260  psrval  21333  neitr  22547  leordtval2  22579  comppfsc  22899  1stckgen  22921  dfac14  22985  ptcmpfi  23180  hausflim  23348  flimclslem  23351  alexsubALTlem2  23415  nmfval  23960  icccmplem2  24202  tcphex  24597  tchnmfval  24608  taylfval  25734  lrrecse  27276  addsval  27296  negsval  27346  negsid  27361  mulsval  27396  mulsproplem10  27410  legval  27568  axlowdimlem15  27947  axlowdim  27952  eengv  27970  uhgrunop  28068  upgrunop  28112  umgrunop  28114  padct  31678  cycpmconjslem2  32046  idlsrgval  32285  ordtconnlem1  32545  sxbrsigalem2  32926  actfunsnf1o  33257  actfunsnrndisj  33258  reprsuc  33268  breprexplema  33283  bnj918  33418  fineqvac  33738  subfacp1lem3  33816  subfacp1lem5  33818  erdszelem8  33832  satfvsuclem1  33993  satf0suc  34010  fmlasuc0  34018  mrexval  34135  mrsubcv  34144  mrsubff  34146  mrsubccat  34152  elmrsubrn  34154  rdgssun  35878  exrecfnlem  35879  finixpnum  36092  poimirlem4  36111  poimirlem15  36122  poimirlem28  36135  rrnval  36315  lsatset  37481  ldualset  37616  pclfinN  38392  dvaset  39497  dvhset  39573  hlhilset  40426  elrfi  41046  istopclsd  41052  mzpcompact2lem  41103  eldioph2lem1  41112  eldioph2lem2  41113  eldioph4b  41163  diophren  41165  ttac  41389  pwslnmlem2  41449  dfacbasgrp  41464  mendval  41539  idomsubgmo  41554  superuncl  41914  ssuncl  41916  sssymdifcl  41918  rclexi  41961  trclexi  41966  rtrclexi  41967  dfrtrcl5  41975  dfrcl2  42020  comptiunov2i  42052  cotrclrcl  42088  frege83  42292  frege110  42319  frege133  42342  clsk1indlem3  42389  fnchoice  43308  limcresiooub  43957  limcresioolb  43958  fourierdlem48  44469  fourierdlem49  44470  fourierdlem102  44523  fourierdlem114  44535  sge0resplit  44721  elpglem2  47231
  Copyright terms: Public domain W3C validator