Theorem un0 4344

Description: The union of a class with the empty set is itself. Dual of inv1 4348. Commuted form of 0un 4346. 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 4284	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfri 953	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 227	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4103	1 ⊢ (𝐴 ∪ ∅) = 𝐴

This proof depends on syntax axioms:   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ∪ cun 3897  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-un 3904  df-nul 4280

This theorem is used by:  0un  4346  un00  4357  csbun  4399  disjssun  4421  difun2  4437  difdifdir  4447  disjpr2  4674  prprc1  4726  diftpsn3  4765  symdif0  5045  symdifid  5047  iununi  5059  unidif0  5321  unidif0OLD  5322  relresdm1  6027  difxp1  6155  difxp2  6156  suc0  6433  sucprc  6434  fresaun  6745  fresaunres2  6746  fvun1  6968  fndifnfp  7173  fvunsn  7176  fvsnun1  7179  fvsnun2  7180  fsnunfv  7184  fsnunres  7185  funiunfv  7244  fnsuppeq0  8193  frrlem12  8299  oev2  8515  oarec  8554  undifixp  8946  domss2  9139  unfi  9170  domunfican  9297  kmlem2  10211  kmlem3  10212  kmlem11  10220  dju0en  10235  djuassen  10238  ackbij1lem1  10278  ackbij1lem13  10290  fin1a2lem10  10468  fin1a2lem12  10470  axdc3lem4  10512  ttukeylem6  10573  alephadd  10643  fpwwe2lem12  10708  indconst1  12314  prunioo  13593  fzsuc2  13696  fseq1p1m1  13712  hashgval  14457  hashinf  14459  hashfun  14562  sadid1  16618  lcmfunsnlem  16796  lcmfun  16800  vdwap1  17135  setsres  17336  setsid  17365  mreexexlem3d  17800  mreexdomd  17803  pwmndid  19122  pwmnd  19123  pwssplit1  21314  lspsnat  21403  lsppratlem3  21407  lindsdom  22136  opsrtoslem2  22345  indistopon  23299  indistps  23309  indistps2  23310  restcld  23470  neitr  23478  refun0  23814  filconn  24182  ufildr  24230  restmetu  24869  ovolioo  25869  itgsplitioo  26138  plyeq0  26510  birthdaylem2  27262  lgsquadlem2  27690  noextendseq  28006  nosupbnd2lem1  28054  noinfbnd2lem1  28069  noetasuplem2  28073  noetasuplem3  28074  noetasuplem4  28075  noetainflem2  28077  bday1  28182  lrold  28265  addsrid  28332  negsproplem2  28397  negsproplem6  28401  muls01  28480  mulsrid  28481  mulsproplem2  28485  mulsproplem3  28486  mulsproplem4  28487  mulsproplem12  28495  mulsproplem13  28496  mulsproplem14  28497  onleft  28628  ltonold  28629  oncutlt  28632  oniso  28639  bdayons  28644  onaddscl  28645  onmulscl  28646  n0cut  28702  n0bday  28720  bdayn0p1  28737  0reno  28864  1reno  28865  ex-dif  31006  ex-in  31008  ex-res  31024  difres  33176  imadifxp  33177  ofpreima2  33242  coprprop  33274  padct  33292  difico  33357  tocycf  33660  tocyc01  33661  elrgspnlem4  33788  esplyind  34189  constrextdg2lem  34362  locfinref  34455  sigaclfu2  34735  prsiga  34745  unelldsys  34773  measun  34826  difelcarsg  34925  carsgclctunlem1  34932  carsggect  34933  eulerpartlemt  34986  eulerpartgbij  34987  ballotlemfp1  35107  fineqvac  35757  indispconn  35968  onint1  37207  bj-pr21val  37896  bj-funun  38141  poimirlem3  38509  poimirlem5  38511  poimirlem10  38516  poimirlem15  38521  poimirlem22  38528  poimirlem23  38529  poimirlem28  38534  padd01  40836  padd02  40837  pclfinclN  40975  mapfzcons1  43681  fzsplit1nn0  43718  diophrw  43723  eldioph2lem1  43724  eldioph2lem2  43725  diophren  43773  pwssplit4  44049  mnuprdlem1  45215  dvmptfprodlem  46898  caratheodorylem1  47480  isomenndlem  47484  fzopredsuc  48338  clnbgr0edg  48879  tposrescnv  49931  tposres2  49932  tposres3  49933  aacllem  50883