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

Theorem unex 7453
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 4820 . 2 {𝐴, 𝐵} = (𝐴𝐵)
4 prex 5301 . . 3 {𝐴, 𝐵} ∈ V
54uniex 7451 . 2 {𝐴, 𝐵} ∈ V
63, 5eqeltrri 2890 1 (𝐴𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  Vcvv 3444  cun 3882  {cpr 4530   cuni 4803
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-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:  tpex  7454  unexb  7455  fvclex  7646  ralxpmap  8447  unen  8583  enfixsn  8613  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  9427  infxpenlem  9428  dfac4  9537  dfac2b  9545  kmlem2  9566  cfsmolem  9685  isfin1-3  9801  axdc2lem  9863  axdc3lem4  9868  axcclem  9872  ttukeylem3  9926  gchac  10096  wunex2  10153  wuncval2  10162  inar1  10190  nn0ex  11895  xrex  12378  seqexw  13384  hashbclem  13810  incexclem  15187  ramub1lem2  16357  prdsval  16724  imasval  16780  ipoval  17760  plusffval  17854  smndex1bas  18067  smndex1sgrp  18069  smndex1mnd  18071  smndex1id  18072  grpinvfval  18138  grpsubfval  18143  mulgfval  18222  staffval  19615  scaffval  19649  lpival  20015  xrsex  20110  ipffval  20341  islindf4  20531  psrval  20604  neitr  21789  leordtval2  21821  comppfsc  22141  1stckgen  22163  dfac14  22227  ptcmpfi  22422  hausflim  22590  flimclslem  22593  alexsubALTlem2  22657  nmfval  23199  icccmplem2  23432  tcphex  23825  tchnmfval  23836  taylfval  24958  legval  26382  axlowdimlem15  26754  axlowdim  26759  eengv  26777  uhgrunop  26872  upgrunop  26916  umgrunop  26918  padct  30485  cycpmconjslem2  30851  idlsrgval  31060  ordtconnlem1  31281  sxbrsigalem2  31658  actfunsnf1o  31989  actfunsnrndisj  31990  reprsuc  32000  breprexplema  32015  bnj918  32151  subfacp1lem3  32543  subfacp1lem5  32545  erdszelem8  32559  satfvsuclem1  32720  satf0suc  32737  fmlasuc0  32745  mrexval  32862  mrsubcv  32871  mrsubff  32873  mrsubccat  32879  elmrsubrn  32881  rdgssun  34796  exrecfnlem  34797  finixpnum  35041  poimirlem4  35060  poimirlem15  35071  poimirlem28  35084  rrnval  35264  lsatset  36285  ldualset  36420  pclfinN  37195  dvaset  38300  dvhset  38376  hlhilset  39229  elrfi  39628  istopclsd  39634  mzpcompact2lem  39685  eldioph2lem1  39694  eldioph2lem2  39695  eldioph4b  39745  diophren  39747  ttac  39970  pwslnmlem2  40030  dfacbasgrp  40045  mendval  40120  idomsubgmo  40135  superuncl  40260  ssuncl  40262  sssymdifcl  40264  rclexi  40308  trclexi  40313  rtrclexi  40314  dfrtrcl5  40322  dfrcl2  40368  comptiunov2i  40400  cotrclrcl  40436  frege83  40640  frege110  40667  frege133  40690  clsk1indlem3  40739  fnchoice  41651  limcresiooub  42277  limcresioolb  42278  fourierdlem48  42789  fourierdlem49  42790  fourierdlem102  42843  fourierdlem114  42855  sge0resplit  43038  elpglem2  45234
  Copyright terms: Public domain W3C validator