Theorem un0 4347

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

This proof depends on syntax axioms:   ∨ wo 861   = wceq 1570   ∈ wcel 2147   ∪ cun 4152  ∅c0 4281

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050  df-un 4154  df-nul 4282

This theorem is used by:  0un  4349  un00  4360  csbun  4402  disjssun  4424  difun2  4440  difdifdir  4450  disjpr2  4674  prprc1  4726  diftpsn3  4765  symdif0  5048  symdifid  5050  iununi  5062  unidif0  5325  unidif0OLD  5326  relresdm1  6037  difxp1  6168  difxp2  6169  suc0  6458  sucprc  6459  fresaun  6775  fresaunres2  6776  fvun1  6999  fndifnfp  7204  fvunsn  7207  fvsnun1  7210  fvsnun2  7211  fsnunfv  7215  fsnunres  7216  funiunfv  7275  fnsuppeq0  8237  frrlem12  8343  oev2  8559  oarec  8598  undifixp  8990  domss2  9183  unfi  9214  domunfican  9341  kmlem2  10257  kmlem3  10258  kmlem11  10266  dju0en  10281  djuassen  10284  ackbij1lem1  10324  ackbij1lem13  10336  fin1a2lem10  10514  fin1a2lem12  10516  axdc3lem4  10558  ttukeylem6  10619  alephadd  10689  fpwwe2lem12  10754  indconst1  12360  prunioo  13639  fzsuc2  13743  fseq1p1m1  13759  hashgval  14504  hashinf  14506  hashfun  14609  sadid1  16667  lcmfunsnlem  16845  lcmfun  16849  vdwap1  17184  setsres  17385  setsid  17414  mreexexlem3d  17849  mreexdomd  17852  pwmndid  19171  pwmnd  19172  pwssplit1  21364  lspsnat  21453  lsppratlem3  21457  lindsdom  22186  opsrtoslem2  22395  indistopon  23349  indistps  23359  indistps2  23360  restcld  23520  neitr  23528  refun0  23864  filconn  24232  ufildr  24280  restmetu  24919  ovolioo  25919  itgsplitioo  26188  plyeq0  26560  birthdaylem2  27310  lgsquadlem2  27738  noextendseq  28054  nosupbnd2lem1  28102  noinfbnd2lem1  28117  noetasuplem2  28121  noetasuplem3  28122  noetasuplem4  28123  noetainflem2  28125  bday1  28230  lrold  28313  addsrid  28380  negsproplem2  28445  negsproplem6  28449  muls01  28528  mulsrid  28529  mulsproplem2  28533  mulsproplem3  28534  mulsproplem4  28535  mulsproplem12  28543  mulsproplem13  28544  mulsproplem14  28545  onleft  28676  ltonold  28677  oncutlt  28680  oniso  28687  bdayons  28692  onaddscl  28693  onmulscl  28694  n0cut  28750  n0bday  28768  bdayn0p1  28785  0reno  28912  1reno  28913  ex-dif  31054  ex-in  31056  ex-res  31072  difres  33266  imadifxp  33267  ofpreima2  33332  coprprop  33363  padct  33381  difico  33445  tocycf  33748  tocyc01  33749  elrgspnlem4  33876  esplyind  34277  constrextdg2lem  34450  locfinref  34543  sigaclfu2  34823  prsiga  34833  unelldsys  34861  measun  34914  difelcarsg  35012  carsgclctunlem1  35019  carsggect  35020  eulerpartlemt  35073  eulerpartgbij  35074  ballotlemfp1  35194  fineqvac  35884  indispconn  36166  onint1  37415  bj-pr21val  38104  bj-funun  38365  poimirlem3  38733  poimirlem5  38735  poimirlem10  38740  poimirlem15  38745  poimirlem22  38752  poimirlem23  38753  poimirlem28  38758  padd01  41060  padd02  41061  pclfinclN  41199  mapfzcons1  43921  fzsplit1nn0  43958  diophrw  43963  eldioph2lem1  43964  eldioph2lem2  43965  diophren  44013  pwssplit4  44284  mnuprdlem1  45448  dvmptfprodlem  47159  caratheodorylem1  47741  isomenndlem  47745  fzopredsuc  48599  clnbgr0edg  49140  tposrescnv  50197  tposres2  50198  tposres3  50199  parhomssun  50952  aacllem  51219