Theorem un0 4344

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 4296	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfi 935	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 226	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4127	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 843   = wceq 1537   ∈ wcel 2114   ∪ cun 3934  ∅c0 4291

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

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-v 3496  df-dif 3939  df-un 3941  df-nul 4292

This theorem is referenced by:  0un  4346  csbun  4390  un00  4394  disjssun  4417  difun2  4429  difdifdir  4437  disjpr2  4649  prprc1  4701  diftpsn3  4735  sspr  4766  sstp  4767  symdif0  5007  symdifv  5008  symdifid  5009  iunxdif3  5017  iununi  5021  unidif0  5260  difxp1  6022  difxp2  6023  suc0  6265  sucprc  6266  fresaun  6549  fresaunres2  6550  fvssunirn  6699  fvun1  6754  fndifnfp  6938  fvunsn  6941  fvsnun1  6944  fvsnun2  6945  fsnunfv  6949  fsnunres  6950  funiunfv  7007  fnsuppeq0  7858  wfrlem14  7968  oev2  8148  oarec  8188  undifixp  8498  domss2  8676  domunfican  8791  kmlem2  9577  kmlem3  9578  kmlem11  9586  dju0en  9601  djuassen  9604  ackbij1lem1  9642  ackbij1lem13  9654  fin1a2lem10  9831  fin1a2lem12  9833  axdc3lem4  9875  ttukeylem6  9936  alephadd  9999  fpwwe2lem13  10064  prunioo  12868  fzsuc2  12966  fseq1p1m1  12982  hashgval  13694  hashinf  13696  hashfun  13799  sadid1  15817  lcmfunsnlem  15985  lcmfun  15989  vdwap1  16313  setsres  16525  setsid  16538  mreexexlem3d  16917  mreexdomd  16920  pwmndid  18101  pwmnd  18102  pwssplit1  19831  lspsnat  19917  lsppratlem3  19921  opsrtoslem2  20265  indistopon  21609  indistps  21619  indistps2  21620  restcld  21780  neitr  21788  refun0  22123  filconn  22491  ufildr  22539  restmetu  23180  ovolioo  24169  itgsplitioo  24438  plyeq0  24801  birthdaylem2  25530  lgsquadlem2  25957  ex-dif  28202  ex-in  28204  ex-res  28220  difres  30350  imadifxp  30351  funresdm1  30355  ofpreima2  30411  coprprop  30435  padct  30455  difico  30506  tocycf  30759  tocyc01  30760  locfinref  31105  sigaclfu2  31380  prsiga  31390  unelldsys  31417  measun  31470  difelcarsg  31568  carsgclctunlem1  31575  carsggect  31576  eulerpartlemt  31629  eulerpartgbij  31630  ballotlemfp1  31749  indispconn  32481  frrlem12  33134  noextendseq  33174  nosupbnd2lem1  33215  noetalem2  33218  noetalem3  33219  onint1  33797  bj-pr21val  34328  bj-funun  34537  lindsdom  34901  poimirlem3  34910  poimirlem5  34912  poimirlem10  34917  poimirlem15  34922  poimirlem22  34929  poimirlem23  34930  poimirlem28  34935  padd01  36962  padd02  36963  pclfinclN  37101  mapfzcons1  39334  fzsplit1nn0  39371  diophrw  39376  eldioph2lem1  39377  eldioph2lem2  39378  diophren  39430  pwssplit4  39709  mnuprdlem1  40628  dvmptfprodlem  42249  caratheodorylem1  42828  isomenndlem  42832  fzopredsuc  43543  aacllem  44922