Theorem un0 4390

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 4330	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfi 937	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 223	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4151	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 845   = wceq 1541   ∈ wcel 2106   ∪ cun 3946  ∅c0 4322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3951  df-un 3953  df-nul 4323

This theorem is referenced by:  0un  4392  csbun  4438  un00  4442  disjssun  4467  difun2  4480  difdifdir  4491  disjpr2  4717  prprc1  4769  diftpsn3  4805  sspr  4836  sstp  4837  symdif0  5088  symdifv  5089  symdifid  5090  iunxdif3  5098  iununi  5102  unidif0  5358  relresdm1  6033  difxp1  6164  difxp2  6165  suc0  6439  sucprc  6440  fresaun  6762  fresaunres2  6763  fvssunirnOLD  6925  fvun1  6982  fndifnfp  7173  fvunsn  7176  fvsnun1  7179  fvsnun2  7180  fsnunfv  7184  fsnunres  7185  funiunfv  7246  fnsuppeq0  8176  frrlem12  8281  wfrlem14OLD  8321  oev2  8522  oarec  8561  undifixp  8927  domss2  9135  unfi  9171  domunfican  9319  kmlem2  10145  kmlem3  10146  kmlem11  10154  dju0en  10169  djuassen  10172  ackbij1lem1  10214  ackbij1lem13  10226  fin1a2lem10  10403  fin1a2lem12  10405  axdc3lem4  10447  ttukeylem6  10508  alephadd  10571  fpwwe2lem12  10636  prunioo  13457  fzsuc2  13558  fseq1p1m1  13574  hashgval  14292  hashinf  14294  hashfun  14396  sadid1  16408  lcmfunsnlem  16577  lcmfun  16581  vdwap1  16909  setsres  17110  setsid  17140  mreexexlem3d  17589  mreexdomd  17592  pwmndid  18816  pwmnd  18817  pwssplit1  20669  lspsnat  20757  lsppratlem3  20761  opsrtoslem2  21616  indistopon  22503  indistps  22513  indistps2  22514  restcld  22675  neitr  22683  refun0  23018  filconn  23386  ufildr  23434  restmetu  24078  ovolioo  25084  itgsplitioo  25354  plyeq0  25724  birthdaylem2  26454  lgsquadlem2  26881  noextendseq  27167  nosupbnd2lem1  27215  noinfbnd2lem1  27230  noetasuplem2  27234  noetasuplem3  27235  noetasuplem4  27236  noetainflem2  27238  bday1s  27329  lrold  27388  addsrid  27445  negsproplem2  27500  negsproplem6  27504  muls01  27565  mulsrid  27566  mulsproplem2  27570  mulsproplem3  27571  mulsproplem4  27572  mulsproplem12  27580  mulsproplem13  27581  mulsproplem14  27582  ex-dif  29673  ex-in  29675  ex-res  29691  difres  31826  imadifxp  31827  ofpreima2  31886  coprprop  31916  padct  31939  difico  31989  tocycf  32271  tocyc01  32272  locfinref  32816  sigaclfu2  33114  prsiga  33124  unelldsys  33151  measun  33204  difelcarsg  33304  carsgclctunlem1  33311  carsggect  33312  eulerpartlemt  33365  eulerpartgbij  33366  ballotlemfp1  33485  fineqvac  34092  indispconn  34220  onint1  35329  bj-pr21val  35889  bj-funun  36128  lindsdom  36477  poimirlem3  36486  poimirlem5  36488  poimirlem10  36493  poimirlem15  36498  poimirlem22  36505  poimirlem23  36506  poimirlem28  36511  padd01  38677  padd02  38678  pclfinclN  38816  metakunt24  41003  mapfzcons1  41445  fzsplit1nn0  41482  diophrw  41487  eldioph2lem1  41488  eldioph2lem2  41489  diophren  41541  pwssplit4  41821  mnuprdlem1  43021  dvmptfprodlem  44650  caratheodorylem1  45232  isomenndlem  45236  fzopredsuc  46021  aacllem  47838