Theorem un0 4360

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 4304	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfri 939	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 224	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4122	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ∪ cun 3915  ∅c0 4299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-un 3922  df-nul 4300

This theorem is referenced by:  0un  4362  csbun  4407  un00  4411  disjssun  4434  difun2  4447  difdifdir  4458  disjpr2  4680  prprc1  4732  diftpsn3  4769  sspr  4802  sstp  4803  symdif0  5052  symdifv  5053  symdifid  5054  iunxdif3  5062  iununi  5066  unidif0  5318  relresdm1  6007  difxp1  6141  difxp2  6142  suc0  6412  sucprc  6413  fresaun  6734  fresaunres2  6735  fvssunirnOLD  6895  fvun1  6955  fndifnfp  7153  fvunsn  7156  fvsnun1  7159  fvsnun2  7160  fsnunfv  7164  fsnunres  7165  funiunfv  7225  fnsuppeq0  8174  frrlem12  8279  oev2  8490  oarec  8529  undifixp  8910  domss2  9106  unfi  9141  domunfican  9279  kmlem2  10112  kmlem3  10113  kmlem11  10121  dju0en  10136  djuassen  10139  ackbij1lem1  10179  ackbij1lem13  10191  fin1a2lem10  10369  fin1a2lem12  10371  axdc3lem4  10413  ttukeylem6  10474  alephadd  10537  fpwwe2lem12  10602  prunioo  13449  fzsuc2  13550  fseq1p1m1  13566  hashgval  14305  hashinf  14307  hashfun  14409  sadid1  16445  lcmfunsnlem  16618  lcmfun  16622  vdwap1  16955  setsres  17155  setsid  17184  mreexexlem3d  17614  mreexdomd  17617  pwmndid  18870  pwmnd  18871  pwssplit1  20973  lspsnat  21062  lsppratlem3  21066  opsrtoslem2  21970  indistopon  22895  indistps  22905  indistps2  22906  restcld  23066  neitr  23074  refun0  23409  filconn  23777  ufildr  23825  restmetu  24465  ovolioo  25476  itgsplitioo  25746  plyeq0  26123  birthdaylem2  26869  lgsquadlem2  27299  noextendseq  27586  nosupbnd2lem1  27634  noinfbnd2lem1  27649  noetasuplem2  27653  noetasuplem3  27654  noetasuplem4  27655  noetainflem2  27657  bday1s  27750  lrold  27815  addsrid  27878  negsproplem2  27942  negsproplem6  27946  muls01  28022  mulsrid  28023  mulsproplem2  28027  mulsproplem3  28028  mulsproplem4  28029  mulsproplem12  28037  mulsproplem13  28038  mulsproplem14  28039  onsleft  28168  sltonold  28169  onscutlt  28172  onsiso  28176  bdayon  28180  onaddscl  28181  onmulscl  28182  n0scut  28233  n0sbday  28251  bdayn0p1  28265  ex-dif  30359  ex-in  30361  ex-res  30377  difres  32536  imadifxp  32537  ofpreima2  32597  coprprop  32629  padct  32650  difico  32713  tocycf  33081  tocyc01  33082  elrgspnlem4  33203  constrextdg2lem  33745  locfinref  33838  sigaclfu2  34118  prsiga  34128  unelldsys  34155  measun  34208  difelcarsg  34308  carsgclctunlem1  34315  carsggect  34316  eulerpartlemt  34369  eulerpartgbij  34370  ballotlemfp1  34490  fineqvac  35094  indispconn  35228  onint1  36444  bj-pr21val  37008  bj-funun  37247  lindsdom  37615  poimirlem3  37624  poimirlem5  37626  poimirlem10  37631  poimirlem15  37636  poimirlem22  37643  poimirlem23  37644  poimirlem28  37649  padd01  39812  padd02  39813  pclfinclN  39951  mapfzcons1  42712  fzsplit1nn0  42749  diophrw  42754  eldioph2lem1  42755  eldioph2lem2  42756  diophren  42808  pwssplit4  43085  mnuprdlem1  44268  dvmptfprodlem  45949  caratheodorylem1  46531  isomenndlem  46535  fzopredsuc  47328  clnbgr0edg  47841  tposrescnv  48871  tposres2  48872  tposres3  48873  aacllem  49794