Theorem unexg 7749

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 3482	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		elex 3482	. 2 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
3		unexb 7748	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V)
4	3	biimpi 215	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V)
5	1, 2, 4	syl2an 594	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2099  Vcvv 3462   ∪ cun 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pr 5425  ax-un 7738

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4323  df-sn 4624  df-pr 4626  df-uni 4906

This theorem is referenced by:  xpexg  7750  unexd  7754  difex2  7760  difsnexi  7761  eldifpw  7768  pwuncl  7770  ordunpr  7827  soex  7926  fnse  8139  suppun  8190  tposexg  8247  frrlem13  8305  wfrlem15OLD  8345  tfrlem12  8411  tfrlem16  8415  elmapresaun  8901  ralxpmap  8917  undifixp  8955  undom  9089  undomOLD  9090  domunsncan  9102  domssex2  9167  domssex  9168  mapunen  9176  sbthfilem  9228  fsuppunbi  9425  elfiun  9466  brwdom2  9609  unwdomg  9620  djuex  9944  djuexALT  9958  alephprc  10135  djudoml  10220  infunabs  10241  fin23lem11  10351  axdc2lem  10482  ttukeylem1  10543  fpwwe2lem12  10676  wunex2  10772  wuncval2  10781  hashunx  14398  hashf1lem1  14468  hashf1lem1OLD  14469  trclexlem  14994  trclun  15014  relexp0g  15022  relexpsucnnr  15025  isstruct2  17146  setsvalg  17163  setsid  17205  yonffth  18304  pwmndgplus  18920  dmdprdsplit2  20042  basdif0  22944  fiuncmp  23396  refun0  23507  ptbasfi  23573  dfac14lem  23609  ptrescn  23631  xkoptsub  23646  filconn  23875  isufil2  23900  ufileu  23911  filufint  23912  fmfnfmlem4  23949  fmfnfm  23950  fclsfnflim  24019  flimfnfcls  24020  ptcmplem1  24044  elply2  26220  plyss  26223  noeta2  27811  etasslt2  27841  scutbdaybnd2lim  27844  wlkp1lem4  29610  resf1o  32644  tocycfv  32991  tocycf  32999  locfinref  33669  esumsplit  33899  esumpad2  33902  sseqval  34235  bnj1149  34650  satfvsuc  35202  satf0suclem  35216  sat1el2xp  35220  fmlasuc0  35225  altxpexg  35815  hfun  36015  refssfne  36083  topjoin  36090  bj-2uplex  36742  ptrest  37333  poimirlem3  37337  paddval  39510  evlselvlem  42276  elrfi  42388  rtrclexlem  43320  clcnvlem  43327  cnvrcl0  43329  dfrtrcl5  43333  iunrelexp0  43406  relexpxpmin  43421  brtrclfv2  43431  sge0resplit  46063  sge0split  46066  setsv  46986  setrec1lem4  48472