Theorem unexg 7106

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

Syntax hints:   → wi 4   ∧ wa 382   ∈ wcel 2145  Vcvv 3351   ∪ cun 3721

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034  ax-un 7096

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-sn 4317  df-pr 4319  df-uni 4575

This theorem is referenced by:  xpexg  7107  difex2  7116  difsnexi  7117  eldifpw  7123  ordunpr  7173  soex  7256  fnse  7445  suppun  7466  tposexg  7518  wfrlem15  7582  tfrlem12  7638  tfrlem16  7642  ralxpmap  8061  undifixp  8098  undom  8204  domunsncan  8216  domssex2  8276  domssex  8277  mapunen  8285  fsuppunbi  8452  elfiun  8492  brwdom2  8634  unwdomg  8645  djuex  8935  djuexALT  8948  alephprc  9122  cdadom3  9212  infunabs  9231  fin23lem11  9341  axdc2lem  9472  ttukeylem1  9533  fpwwe2lem13  9666  wunex2  9762  wuncval2  9771  hashunx  13377  hashf1lem1  13441  trclexlem  13943  trclun  13963  relexp0g  13970  relexpsucnnr  13973  isstruct2  16074  setsvalg  16094  setsid  16121  yonffth  17132  dmdprdsplit2  18653  basdif0  20978  fiuncmp  21428  refun0  21539  ptbasfi  21605  dfac14lem  21641  ptrescn  21663  xkoptsub  21678  filconn  21907  isufil2  21932  ufileu  21943  filufint  21944  fmfnfmlem4  21981  fmfnfm  21982  fclsfnflim  22051  flimfnfcls  22052  ptcmplem1  22076  elply2  24172  plyss  24175  wlkp1lem4  26808  resf1o  29845  locfinref  30248  esumsplit  30455  esumpad2  30458  sseqval  30790  bnj1149  31201  ssltun1  32252  ssltun2  32253  altxpexg  32422  hfun  32622  refssfne  32690  topjoin  32697  bj-2uplex  33341  cnfinltrel  33578  ptrest  33741  poimirlem3  33745  paddval  35606  elrfi  37783  elmapresaun  37860  rclexi  38448  rtrclexlem  38449  trclubgNEW  38451  clcnvlem  38456  cnvrcl0  38458  dfrtrcl5  38462  iunrelexp0  38520  relexpmulg  38528  relexp01min  38531  relexpxpmin  38535  brtrclfv2  38545  sge0resplit  41140  sge0split  41143  setsv  41876  setrec1lem4  42965