Theorem un0 4347

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-dif 3908  df-un 3910  df-nul 4287

This theorem is referenced by:  0un  4349  csbun  4394  un00  4398  disjssun  4421  difun2  4434  difdifdir  4445  disjpr2  4667  prprc1  4719  diftpsn3  4756  sspr  4789  sstp  4790  symdif0  5037  symdifv  5038  symdifid  5039  iunxdif3  5047  iununi  5051  unidif0  5302  relresdm1  5988  difxp1  6118  difxp2  6119  suc0  6388  sucprc  6389  fresaun  6699  fresaunres2  6700  fvssunirnOLD  6858  fvun1  6918  fndifnfp  7116  fvunsn  7119  fvsnun1  7122  fvsnun2  7123  fsnunfv  7127  fsnunres  7128  funiunfv  7188  fnsuppeq0  8132  frrlem12  8237  oev2  8448  oarec  8487  undifixp  8868  domss2  9060  unfi  9095  domunfican  9230  kmlem2  10065  kmlem3  10066  kmlem11  10074  dju0en  10089  djuassen  10092  ackbij1lem1  10132  ackbij1lem13  10144  fin1a2lem10  10322  fin1a2lem12  10324  axdc3lem4  10366  ttukeylem6  10427  alephadd  10490  fpwwe2lem12  10555  prunioo  13402  fzsuc2  13503  fseq1p1m1  13519  hashgval  14258  hashinf  14260  hashfun  14362  sadid1  16397  lcmfunsnlem  16570  lcmfun  16574  vdwap1  16907  setsres  17107  setsid  17136  mreexexlem3d  17570  mreexdomd  17573  pwmndid  18828  pwmnd  18829  pwssplit1  20981  lspsnat  21070  lsppratlem3  21074  opsrtoslem2  21979  indistopon  22904  indistps  22914  indistps2  22915  restcld  23075  neitr  23083  refun0  23418  filconn  23786  ufildr  23834  restmetu  24474  ovolioo  25485  itgsplitioo  25755  plyeq0  26132  birthdaylem2  26878  lgsquadlem2  27308  noextendseq  27595  nosupbnd2lem1  27643  noinfbnd2lem1  27658  noetasuplem2  27662  noetasuplem3  27663  noetasuplem4  27664  noetainflem2  27666  bday1s  27763  lrold  27829  addsrid  27894  negsproplem2  27958  negsproplem6  27962  muls01  28038  mulsrid  28039  mulsproplem2  28043  mulsproplem3  28044  mulsproplem4  28045  mulsproplem12  28053  mulsproplem13  28054  mulsproplem14  28055  onsleft  28184  sltonold  28185  onscutlt  28188  onsiso  28192  bdayon  28196  onaddscl  28197  onmulscl  28198  n0scut  28249  n0sbday  28267  bdayn0p1  28281  ex-dif  30385  ex-in  30387  ex-res  30403  difres  32562  imadifxp  32563  ofpreima2  32623  coprprop  32655  padct  32676  difico  32739  tocycf  33072  tocyc01  33073  elrgspnlem4  33195  constrextdg2lem  33714  locfinref  33807  sigaclfu2  34087  prsiga  34097  unelldsys  34124  measun  34177  difelcarsg  34277  carsgclctunlem1  34284  carsggect  34285  eulerpartlemt  34338  eulerpartgbij  34339  ballotlemfp1  34459  fineqvac  35071  indispconn  35206  onint1  36422  bj-pr21val  36986  bj-funun  37225  lindsdom  37593  poimirlem3  37602  poimirlem5  37604  poimirlem10  37609  poimirlem15  37614  poimirlem22  37621  poimirlem23  37622  poimirlem28  37627  padd01  39790  padd02  39791  pclfinclN  39929  mapfzcons1  42690  fzsplit1nn0  42727  diophrw  42732  eldioph2lem1  42733  eldioph2lem2  42734  diophren  42786  pwssplit4  43062  mnuprdlem1  44245  dvmptfprodlem  45926  caratheodorylem1  46508  isomenndlem  46512  fzopredsuc  47308  clnbgr0edg  47822  tposrescnv  48864  tposres2  48865  tposres3  48866  aacllem  49787