Theorem unexg 7736

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

Step	Hyp	Ref	Expression
1		elex 3493	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		elex 3493	. 2 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
3		unexb 7735	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V)
4	3	biimpi 215	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V)
5	1, 2, 4	syl2an 597	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  Vcvv 3475   ∪ cun 3947

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 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725

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 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-sn 4630  df-pr 4632  df-uni 4910

This theorem is referenced by:  xpexg  7737  unexd  7741  difex2  7747  difsnexi  7748  eldifpw  7755  pwuncl  7757  ordunpr  7814  soex  7912  fnse  8119  suppun  8169  tposexg  8225  frrlem13  8283  wfrlem15OLD  8323  tfrlem12  8389  tfrlem16  8393  elmapresaun  8874  ralxpmap  8890  undifixp  8928  undom  9059  undomOLD  9060  domunsncan  9072  domssex2  9137  domssex  9138  mapunen  9146  sbthfilem  9201  fsuppunbi  9384  elfiun  9425  brwdom2  9568  unwdomg  9579  djuex  9903  djuexALT  9917  alephprc  10094  djudoml  10179  infunabs  10202  fin23lem11  10312  axdc2lem  10443  ttukeylem1  10504  fpwwe2lem12  10637  wunex2  10733  wuncval2  10742  hashunx  14346  hashf1lem1  14415  hashf1lem1OLD  14416  trclexlem  14941  trclun  14961  relexp0g  14969  relexpsucnnr  14972  isstruct2  17082  setsvalg  17099  setsid  17141  yonffth  18237  pwmndgplus  18816  dmdprdsplit2  19916  basdif0  22456  fiuncmp  22908  refun0  23019  ptbasfi  23085  dfac14lem  23121  ptrescn  23143  xkoptsub  23158  filconn  23387  isufil2  23412  ufileu  23423  filufint  23424  fmfnfmlem4  23461  fmfnfm  23462  fclsfnflim  23531  flimfnfcls  23532  ptcmplem1  23556  elply2  25710  plyss  25713  noeta2  27286  etasslt2  27315  scutbdaybnd2lim  27318  wlkp1lem4  28933  resf1o  31955  tocycfv  32268  tocycf  32276  locfinref  32821  esumsplit  33051  esumpad2  33054  sseqval  33387  bnj1149  33803  satfvsuc  34352  satf0suclem  34366  sat1el2xp  34370  fmlasuc0  34375  altxpexg  34950  hfun  35150  refssfne  35243  topjoin  35250  bj-2uplex  35903  ptrest  36487  poimirlem3  36491  paddval  38669  evlselvlem  41158  elrfi  41432  rtrclexlem  42367  clcnvlem  42374  cnvrcl0  42376  dfrtrcl5  42380  iunrelexp0  42453  relexpxpmin  42468  brtrclfv2  42478  sge0resplit  45122  sge0split  45125  setsv  46046  setrec1lem4  47735