Theorem un0 4329

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 4273	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfri 945	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 225	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4093	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 853   = wceq 1547   ∈ wcel 2119   ∪ cun 3888  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-dif 3893  df-un 3895  df-nul 4269

This theorem is referenced by:  0un  4331  csbun  4376  un00  4380  disjssun  4403  difun2  4416  difdifdir  4426  disjpr2  4652  prprc1  4704  diftpsn3  4742  symdif0  5021  symdifid  5023  iununi  5035  unidif0  5295  unidif0OLD  5296  relresdm1  5992  difxp1  6123  difxp2  6124  suc0  6394  sucprc  6395  fresaun  6705  fresaunres2  6706  fvun1  6925  fndifnfp  7127  fvunsn  7130  fvsnun1  7133  fvsnun2  7134  fsnunfv  7138  fsnunres  7139  funiunfv  7199  fnsuppeq0  8139  frrlem12  8244  oev2  8455  oarec  8494  undifixp  8879  domss2  9071  unfi  9102  domunfican  9229  kmlem2  10072  kmlem3  10073  kmlem11  10081  dju0en  10096  djuassen  10099  ackbij1lem1  10139  ackbij1lem13  10151  fin1a2lem10  10329  fin1a2lem12  10331  axdc3lem4  10373  ttukeylem6  10434  alephadd  10498  fpwwe2lem12  10563  indconst1  12170  prunioo  13432  fzsuc2  13534  fseq1p1m1  13550  hashgval  14293  hashinf  14295  hashfun  14397  sadid1  16435  lcmfunsnlem  16608  lcmfun  16612  vdwap1  16946  setsres  17146  setsid  17175  mreexexlem3d  17610  mreexdomd  17613  pwmndid  18905  pwmnd  18906  pwssplit1  21056  lspsnat  21145  lsppratlem3  21149  opsrtoslem2  22039  indistopon  22991  indistps  23001  indistps2  23002  restcld  23162  neitr  23170  refun0  23505  filconn  23873  ufildr  23921  restmetu  24560  ovolioo  25560  itgsplitioo  25830  plyeq0  26201  birthdaylem2  26941  lgsquadlem2  27369  noextendseq  27656  nosupbnd2lem1  27704  noinfbnd2lem1  27719  noetasuplem2  27723  noetasuplem3  27724  noetasuplem4  27725  noetainflem2  27727  bday1  27831  lrold  27914  addsrid  27981  negsproplem2  28046  negsproplem6  28050  muls01  28129  mulsrid  28130  mulsproplem2  28134  mulsproplem3  28135  mulsproplem4  28136  mulsproplem12  28144  mulsproplem13  28145  mulsproplem14  28146  onleft  28277  ltonold  28278  oncutlt  28281  oniso  28288  bdayons  28293  onaddscl  28294  onmulscl  28295  n0cut  28351  n0bday  28369  bdayn0p1  28386  0reno  28513  1reno  28514  ex-dif  30518  ex-in  30520  ex-res  30536  difres  32696  imadifxp  32697  ofpreima2  32765  coprprop  32798  padct  32817  difico  32882  tocycf  33205  tocyc01  33206  elrgspnlem4  33333  esplyind  33766  constrextdg2lem  33939  locfinref  34032  sigaclfu2  34312  prsiga  34322  unelldsys  34349  measun  34402  difelcarsg  34501  carsgclctunlem1  34508  carsggect  34509  eulerpartlemt  34562  eulerpartgbij  34563  ballotlemfp1  34683  fineqvac  35304  indispconn  35469  onint1  36684  bj-pr21val  37373  bj-funun  37619  lindsdom  37988  poimirlem3  37997  poimirlem5  37999  poimirlem10  38004  poimirlem15  38009  poimirlem22  38016  poimirlem23  38017  poimirlem28  38022  padd01  40310  padd02  40311  pclfinclN  40449  mapfzcons1  43173  fzsplit1nn0  43210  diophrw  43215  eldioph2lem1  43216  eldioph2lem2  43217  diophren  43265  pwssplit4  43541  mnuprdlem1  44723  dvmptfprodlem  46394  caratheodorylem1  46976  isomenndlem  46980  fzopredsuc  47794  clnbgr0edg  48335  tposrescnv  49376  tposres2  49377  tposres3  49378  aacllem  50298