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

Theorem unex 7458
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 4843 . 2 {𝐴, 𝐵} = (𝐴𝐵)
4 prex 5323 . . 3 {𝐴, 𝐵} ∈ V
54uniex 7454 . 2 {𝐴, 𝐵} ∈ V
63, 5eqeltrri 2907 1 (𝐴𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  Vcvv 3492  cun 3931  {cpr 4559   cuni 4830
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-v 3494  df-dif 3936  df-un 3938  df-nul 4289  df-sn 4558  df-pr 4560  df-uni 4831
This theorem is referenced by:  tpex  7459  unexb  7460  fvclex  7649  ralxpmap  8448  unen  8584  enfixsn  8614  sbthlem10  8624  unxpdomlem3  8712  isinf  8719  findcard2  8746  ac6sfi  8750  pwfilem  8806  cnfcomlem  9150  trcl  9158  tc2  9172  rankxpu  9293  rankxplim  9296  rankxplim3  9298  r0weon  9426  infxpenlem  9427  dfac4  9536  dfac2b  9544  kmlem2  9565  cfsmolem  9680  isfin1-3  9796  axdc2lem  9858  axdc3lem4  9863  axcclem  9867  ttukeylem3  9921  gchac  10091  wunex2  10148  wuncval2  10157  inar1  10185  nn0ex  11891  xrex  12374  seqexw  13373  hashbclem  13798  incexclem  15179  ramub1lem2  16351  prdsval  16716  imasval  16772  ipoval  17752  plusffval  17846  grpinvfval  18080  grpsubfval  18085  mulgfval  18164  staffval  19547  scaffval  19581  lpival  19946  psrval  20070  xrsex  20488  ipffval  20720  islindf4  20910  neitr  21716  leordtval2  21748  comppfsc  22068  1stckgen  22090  dfac14  22154  ptcmpfi  22349  hausflim  22517  flimclslem  22520  alexsubALTlem2  22584  nmfval  23125  icccmplem2  23358  tcphex  23747  tchnmfval  23758  taylfval  24874  legval  26297  axlowdimlem15  26669  axlowdim  26674  eengv  26692  uhgrunop  26787  upgrunop  26831  umgrunop  26833  padct  30381  cycpmconjslem2  30724  ordtconnlem1  31066  sxbrsigalem2  31443  actfunsnf1o  31774  actfunsnrndisj  31775  reprsuc  31785  breprexplema  31800  bnj918  31936  subfacp1lem3  32326  subfacp1lem5  32328  erdszelem8  32342  satfvsuclem1  32503  satf0suc  32520  fmlasuc0  32528  mrexval  32645  mrsubcv  32654  mrsubff  32656  mrsubccat  32662  elmrsubrn  32664  rdgssun  34541  exrecfnlem  34542  finixpnum  34758  poimirlem4  34777  poimirlem15  34788  poimirlem28  34801  rrnval  34986  lsatset  36006  ldualset  36141  pclfinN  36916  dvaset  38021  dvhset  38097  hlhilset  38950  elrfi  39169  istopclsd  39175  mzpcompact2lem  39226  eldioph2lem1  39235  eldioph2lem2  39236  eldioph4b  39286  diophren  39288  ttac  39511  pwslnmlem2  39571  dfacbasgrp  39586  mendval  39661  idomsubgmo  39676  superuncl  39805  ssuncl  39807  sssymdifcl  39809  rclexi  39853  trclexi  39858  rtrclexi  39859  dfrtrcl5  39867  dfrcl2  39897  comptiunov2i  39929  cotrclrcl  39965  frege83  40170  frege110  40197  frege133  40220  clsk1indlem3  40271  fnchoice  41163  limcresiooub  41799  limcresioolb  41800  fourierdlem48  42316  fourierdlem49  42317  fourierdlem102  42370  fourierdlem114  42382  sge0resplit  42565  smndex1bas  44006  smndex1sgrp  44008  smndex1mnd  44010  smndex1id  44011  elpglem2  44742
  Copyright terms: Public domain W3C validator