Theorem unexg 7472

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  Vcvv 3494   ∪ cun 3934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-sn 4568  df-pr 4570  df-uni 4839

This theorem is referenced by:  xpexg  7473  difex2  7482  difsnexi  7483  eldifpw  7490  pwuncl  7492  ordunpr  7541  soex  7626  fnse  7827  suppun  7850  tposexg  7906  wfrlem15  7969  tfrlem12  8025  tfrlem16  8029  elmapresaun  8444  ralxpmap  8460  undifixp  8498  undom  8605  domunsncan  8617  domssex2  8677  domssex  8678  mapunen  8686  fsuppunbi  8854  elfiun  8894  brwdom2  9037  unwdomg  9048  djuex  9337  djuexALT  9351  alephprc  9525  djudoml  9610  infunabs  9629  fin23lem11  9739  axdc2lem  9870  ttukeylem1  9931  fpwwe2lem13  10064  wunex2  10160  wuncval2  10169  hashunx  13748  hashf1lem1  13814  trclexlem  14354  trclun  14374  relexp0g  14381  relexpsucnnr  14384  isstruct2  16493  setsvalg  16512  setsid  16538  yonffth  17534  pwmndgplus  18100  dmdprdsplit2  19168  basdif0  21561  fiuncmp  22012  refun0  22123  ptbasfi  22189  dfac14lem  22225  ptrescn  22247  xkoptsub  22262  filconn  22491  isufil2  22516  ufileu  22527  filufint  22528  fmfnfmlem4  22565  fmfnfm  22566  fclsfnflim  22635  flimfnfcls  22636  ptcmplem1  22660  elply2  24786  plyss  24789  wlkp1lem4  27458  resf1o  30466  tocycfv  30751  tocycf  30759  locfinref  31105  esumsplit  31312  esumpad2  31315  sseqval  31646  bnj1149  32064  satfvsuc  32608  satf0suclem  32622  sat1el2xp  32626  fmlasuc0  32631  frrlem13  33135  ssltun1  33269  ssltun2  33270  altxpexg  33439  hfun  33639  refssfne  33706  topjoin  33713  bj-2uplex  34337  ptrest  34906  poimirlem3  34910  paddval  36949  elrfi  39311  rclexi  39995  rtrclexlem  39996  trclubgNEW  39998  clcnvlem  40003  cnvrcl0  40005  dfrtrcl5  40009  iunrelexp0  40067  relexpmulg  40075  relexp01min  40078  relexpxpmin  40082  brtrclfv2  40092  sge0resplit  42708  sge0split  42711  setsv  43558  setrec1lem4  44813