Theorem un0 3919

Description: The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 15-Jul-1993.)

Assertion

Ref	Expression
un0	⊢ (𝐴 ∪ ∅) = 𝐴

Proof of Theorem un0

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 3878	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfi 421	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 213	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 3717	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 382   = wceq 1475   ∈ wcel 1977   ∪ cun 3538  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-un 3545  df-nul 3875

This theorem is referenced by:  csbun  3961  un00  3963  disjssun  3988  difun2  4000  difdifdir  4008  disjpr2  4194  disjpr2OLD  4195  prprc1  4243  diftpsn3  4273  diftpsn3OLD  4274  sspr  4306  sstp  4307  symdif0  4533  symdifv  4534  symdifid  4535  iunxdif3  4542  iununi  4546  unidif0  4764  difxp1  5478  difxp2  5479  suc0  5716  sucprc  5717  fresaun  5988  fresaunres2  5989  fvssunirn  6127  fvun1  6179  fndifnfp  6347  fvunsn  6350  fvsnun1  6353  fvsnun2  6354  fsnunfv  6358  fsnunres  6359  funiunfv  6410  fnsuppeq0  7210  wfrlem14  7315  oev2  7490  oarec  7529  undifixp  7830  domss2  8004  domunfican  8118  kmlem2  8856  kmlem3  8857  kmlem11  8865  cda0en  8884  cdaassen  8887  ackbij1lem1  8925  ackbij1lem13  8937  fin1a2lem10  9114  fin1a2lem12  9116  axdc3lem4  9158  ttukeylem6  9219  alephadd  9278  fpwwe2lem13  9343  prunioo  12172  fzsuc2  12268  fseq1p1m1  12283  hashgval  12982  hashinf  12984  hashfun  13084  sadid1  15028  lcmfunsnlem  15192  lcmfun  15196  vdwap1  15519  setsres  15729  setsid  15742  mreexexlem3d  16129  mreexdomd  16133  pwssplit1  18880  lspsnat  18966  lsppratlem3  18970  opsrtoslem2  19306  indistopon  20615  indistps  20625  indistps2  20626  restcld  20786  neitr  20794  refun0  21128  filcon  21497  ufildr  21545  restmetu  22185  ovolioo  23143  itgsplitioo  23410  plyeq0  23771  birthdaylem2  24479  lgsquadlem2  24906  constr3pthlem1  26183  ex-dif  26672  ex-in  26674  ex-res  26690  difres  28795  imadifxp  28796  ofpreima2  28849  padct  28885  difico  28935  locfinref  29236  sigaclfu2  29511  prsiga  29521  unelldsys  29548  measun  29601  difelcarsg  29699  carsgclctunlem1  29706  carsggect  29707  eulerpartlemt  29760  eulerpartgbij  29761  ballotlemfp1  29880  indispcon  30470  nofulllem1  31101  nofulllem2  31102  onint1  31618  bj-pr21val  32194  bj-pr22val  32200  lindsdom  32573  poimirlem3  32582  poimirlem5  32584  poimirlem10  32589  poimirlem15  32594  poimirlem22  32601  poimirlem23  32602  poimirlem28  32607  padd01  34115  padd02  34116  pclfinclN  34254  mapfzcons1  36298  fzsplit1nn0  36335  diophrw  36340  eldioph2lem1  36341  eldioph2lem2  36342  diophren  36395  pwssplit4  36677  0un  38240  dvmptfprodlem  38834  prsal  39214  caratheodorylem1  39416  isomenndlem  39420  fzopredsuc  39946  aacllem  42356