Theorem un0 4352

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

Syntax hints:   ∨ wo 860   = wceq 1570   ∈ wcel 2143   ∪ cun 3904  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3909  df-un 3911  df-nul 4288

This theorem is referenced by:  0un  4354  un00  4365  csbun  4407  disjssun  4429  difun2  4443  difdifdir  4453  disjpr2  4680  prprc1  4732  diftpsn3  4771  symdif0  5052  symdifid  5054  iununi  5066  unidif0  5332  unidif0OLD  5333  relresdm1  6037  difxp1  6164  difxp2  6165  suc0  6440  sucprc  6441  fresaun  6751  fresaunres2  6752  fvun1  6974  fndifnfp  7176  fvunsn  7179  fvsnun1  7182  fvsnun2  7183  fsnunfv  7187  fsnunres  7188  funiunfv  7248  fnsuppeq0  8189  frrlem12  8295  oev2  8509  oarec  8548  undifixp  8933  domss2  9125  unfi  9156  domunfican  9282  kmlem2  10136  kmlem3  10137  kmlem11  10145  dju0en  10160  djuassen  10163  ackbij1lem1  10203  ackbij1lem13  10215  fin1a2lem10  10394  fin1a2lem12  10396  axdc3lem4  10438  ttukeylem6  10499  alephadd  10563  fpwwe2lem12  10628  indconst1  12232  prunioo  13509  fzsuc2  13612  fseq1p1m1  13628  hashgval  14371  hashinf  14373  hashfun  14476  sadid1  16527  lcmfunsnlem  16700  lcmfun  16704  vdwap1  17038  setsres  17239  setsid  17268  mreexexlem3d  17703  mreexdomd  17706  pwmndid  18999  pwmnd  19000  pwssplit1  21161  lspsnat  21250  lsppratlem3  21254  opsrtoslem2  22188  indistopon  23139  indistps  23149  indistps2  23150  restcld  23310  neitr  23318  refun0  23653  filconn  24021  ufildr  24069  restmetu  24708  ovolioo  25708  itgsplitioo  25978  plyeq0  26349  birthdaylem2  27095  lgsquadlem2  27523  noextendseq  27809  nosupbnd2lem1  27857  noinfbnd2lem1  27872  noetasuplem2  27876  noetasuplem3  27877  noetasuplem4  27878  noetainflem2  27880  bday1  27985  lrold  28068  addsrid  28135  negsproplem2  28200  negsproplem6  28204  muls01  28283  mulsrid  28284  mulsproplem2  28288  mulsproplem3  28289  mulsproplem4  28290  mulsproplem12  28298  mulsproplem13  28299  mulsproplem14  28300  onleft  28431  ltonold  28432  oncutlt  28435  oniso  28442  bdayons  28447  onaddscl  28448  onmulscl  28449  n0cut  28505  n0bday  28523  bdayn0p1  28540  0reno  28667  1reno  28668  ex-dif  30752  ex-in  30754  ex-res  30770  difres  32923  imadifxp  32924  ofpreima2  32989  coprprop  33022  padct  33041  difico  33106  tocycf  33415  tocyc01  33416  elrgspnlem4  33543  esplyind  33943  constrextdg2lem  34116  locfinref  34209  sigaclfu2  34489  prsiga  34499  unelldsys  34526  measun  34579  difelcarsg  34678  carsgclctunlem1  34685  carsggect  34686  eulerpartlemt  34739  eulerpartgbij  34740  ballotlemfp1  34860  fineqvac  35507  indispconn  35704  onint1  36938  bj-pr21val  37627  bj-funun  37874  lindsdom  38243  poimirlem3  38252  poimirlem5  38254  poimirlem10  38259  poimirlem15  38264  poimirlem22  38271  poimirlem23  38272  poimirlem28  38277  padd01  40563  padd02  40564  pclfinclN  40702  mapfzcons1  43428  fzsplit1nn0  43465  diophrw  43470  eldioph2lem1  43471  eldioph2lem2  43472  diophren  43520  pwssplit4  43796  mnuprdlem1  44962  dvmptfprodlem  46638  caratheodorylem1  47220  isomenndlem  47224  fzopredsuc  48038  clnbgr0edg  48579  tposrescnv  49634  tposres2  49635  tposres3  49636  aacllem  50578