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

Syntax hints:   ∨ wo 858   = wceq 1559   ∈ wcel 2141   ∪ cun 3902  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3907  df-un 3909  df-nul 4286

This theorem is referenced by:  0un  4349  csbun  4394  un00  4398  disjssun  4421  difun2  4434  difdifdir  4444  disjpr2  4671  prprc1  4723  diftpsn3  4761  symdif0  5041  symdifid  5043  iununi  5055  unidif0  5315  unidif0OLD  5316  relresdm1  6019  difxp1  6147  difxp2  6148  suc0  6419  sucprc  6420  fresaun  6731  fresaunres2  6732  fvun1  6954  fndifnfp  7156  fvunsn  7159  fvsnun1  7162  fvsnun2  7163  fsnunfv  7167  fsnunres  7168  funiunfv  7228  fnsuppeq0  8167  frrlem12  8273  oev2  8487  oarec  8526  undifixp  8912  domss2  9104  unfi  9135  domunfican  9262  kmlem2  10105  kmlem3  10106  kmlem11  10114  dju0en  10129  djuassen  10132  ackbij1lem1  10172  ackbij1lem13  10184  fin1a2lem10  10363  fin1a2lem12  10365  axdc3lem4  10407  ttukeylem6  10468  alephadd  10532  fpwwe2lem12  10597  indconst1  12205  prunioo  13482  fzsuc2  13584  fseq1p1m1  13600  hashgval  14343  hashinf  14345  hashfun  14447  sadid1  16485  lcmfunsnlem  16658  lcmfun  16662  vdwap1  16996  setsres  17197  setsid  17226  mreexexlem3d  17661  mreexdomd  17664  pwmndid  18956  pwmnd  18957  pwssplit1  21106  lspsnat  21195  lsppratlem3  21199  opsrtoslem2  22089  indistopon  23041  indistps  23051  indistps2  23052  restcld  23212  neitr  23220  refun0  23555  filconn  23923  ufildr  23971  restmetu  24610  ovolioo  25610  itgsplitioo  25880  plyeq0  26251  birthdaylem2  26994  lgsquadlem2  27422  noextendseq  27708  nosupbnd2lem1  27756  noinfbnd2lem1  27771  noetasuplem2  27775  noetasuplem3  27776  noetasuplem4  27777  noetainflem2  27779  bday1  27884  lrold  27967  addsrid  28034  negsproplem2  28099  negsproplem6  28103  muls01  28182  mulsrid  28183  mulsproplem2  28187  mulsproplem3  28188  mulsproplem4  28189  mulsproplem12  28197  mulsproplem13  28198  mulsproplem14  28199  onleft  28330  ltonold  28331  oncutlt  28334  oniso  28341  bdayons  28346  onaddscl  28347  onmulscl  28348  n0cut  28404  n0bday  28422  bdayn0p1  28439  0reno  28566  1reno  28567  ex-dif  30571  ex-in  30573  ex-res  30589  difres  32749  imadifxp  32750  ofpreima2  32818  coprprop  32851  padct  32870  difico  32935  tocycf  33258  tocyc01  33259  elrgspnlem4  33387  esplyind  33833  constrextdg2lem  34006  locfinref  34099  sigaclfu2  34379  prsiga  34389  unelldsys  34416  measun  34469  difelcarsg  34568  carsgclctunlem1  34575  carsggect  34576  eulerpartlemt  34629  eulerpartgbij  34630  ballotlemfp1  34750  fineqvac  35376  indispconn  35548  onint1  36773  bj-pr21val  37462  bj-funun  37708  lindsdom  38077  poimirlem3  38086  poimirlem5  38088  poimirlem10  38093  poimirlem15  38098  poimirlem22  38105  poimirlem23  38106  poimirlem28  38111  padd01  40399  padd02  40400  pclfinclN  40538  mapfzcons1  43262  fzsplit1nn0  43299  diophrw  43304  eldioph2lem1  43305  eldioph2lem2  43306  diophren  43354  pwssplit4  43630  mnuprdlem1  44812  dvmptfprodlem  46482  caratheodorylem1  47064  isomenndlem  47068  fzopredsuc  47882  clnbgr0edg  48423  tposrescnv  49464  tposres2  49465  tposres3  49466  aacllem  50386