Theorem un0 4354

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

This proof depends on syntax axioms:   ∨ wo 861   = wceq 1570   ∈ wcel 2146   ∪ cun 3906  ∅c0 4289

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-dif 3911  df-un 3913  df-nul 4290

This theorem is used by:  0un  4356  un00  4367  csbun  4409  disjssun  4431  difun2  4447  difdifdir  4457  disjpr2  4684  prprc1  4736  diftpsn3  4775  symdif0  5056  symdifid  5058  iununi  5070  unidif0  5335  unidif0OLD  5336  relresdm1  6040  difxp1  6167  difxp2  6168  suc0  6445  sucprc  6446  fresaun  6756  fresaunres2  6757  fvun1  6979  fndifnfp  7181  fvunsn  7184  fvsnun1  7187  fvsnun2  7188  fsnunfv  7192  fsnunres  7193  funiunfv  7253  fnsuppeq0  8197  frrlem12  8303  oev2  8517  oarec  8556  undifixp  8941  domss2  9134  unfi  9165  domunfican  9291  kmlem2  10154  kmlem3  10155  kmlem11  10163  dju0en  10178  djuassen  10181  ackbij1lem1  10221  ackbij1lem13  10233  fin1a2lem10  10411  fin1a2lem12  10413  axdc3lem4  10455  ttukeylem6  10516  alephadd  10580  fpwwe2lem12  10645  indconst1  12249  prunioo  13526  fzsuc2  13629  fseq1p1m1  13645  hashgval  14389  hashinf  14391  hashfun  14494  sadid1  16551  lcmfunsnlem  16724  lcmfun  16728  vdwap1  17062  setsres  17263  setsid  17292  mreexexlem3d  17727  mreexdomd  17730  pwmndid  19029  pwmnd  19030  pwssplit1  21217  lspsnat  21306  lsppratlem3  21310  opsrtoslem2  22244  indistopon  23195  indistps  23205  indistps2  23206  restcld  23366  neitr  23374  refun0  23709  filconn  24077  ufildr  24125  restmetu  24764  ovolioo  25764  itgsplitioo  26034  plyeq0  26405  birthdaylem2  27154  lgsquadlem2  27582  noextendseq  27868  nosupbnd2lem1  27916  noinfbnd2lem1  27931  noetasuplem2  27935  noetasuplem3  27936  noetasuplem4  27937  noetainflem2  27939  bday1  28044  lrold  28127  addsrid  28194  negsproplem2  28259  negsproplem6  28263  muls01  28342  mulsrid  28343  mulsproplem2  28347  mulsproplem3  28348  mulsproplem4  28349  mulsproplem12  28357  mulsproplem13  28358  mulsproplem14  28359  onleft  28490  ltonold  28491  oncutlt  28494  oniso  28501  bdayons  28506  onaddscl  28507  onmulscl  28508  n0cut  28564  n0bday  28582  bdayn0p1  28599  0reno  28726  1reno  28727  ex-dif  30811  ex-in  30813  ex-res  30829  difres  32982  imadifxp  32983  ofpreima2  33048  coprprop  33081  padct  33100  difico  33165  tocycf  33468  tocyc01  33469  elrgspnlem4  33596  esplyind  33996  constrextdg2lem  34169  locfinref  34262  sigaclfu2  34542  prsiga  34552  unelldsys  34579  measun  34632  difelcarsg  34731  carsgclctunlem1  34738  carsggect  34739  eulerpartlemt  34792  eulerpartgbij  34793  ballotlemfp1  34913  fineqvac  35552  indispconn  35746  onint1  37000  bj-pr21val  37689  bj-funun  37936  lindsdom  38305  poimirlem3  38314  poimirlem5  38316  poimirlem10  38321  poimirlem15  38326  poimirlem22  38333  poimirlem23  38334  poimirlem28  38339  padd01  40625  padd02  40626  pclfinclN  40764  mapfzcons1  43488  fzsplit1nn0  43525  diophrw  43530  eldioph2lem1  43531  eldioph2lem2  43532  diophren  43580  pwssplit4  43856  mnuprdlem1  45022  dvmptfprodlem  46698  caratheodorylem1  47280  isomenndlem  47284  fzopredsuc  48101  clnbgr0edg  48642  tposrescnv  49697  tposres2  49698  tposres3  49699  aacllem  50661