Theorem un0 4343

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

This proof depends on syntax axioms:   ∨ wo 861   = wceq 1569   ∈ wcel 2144   ∪ cun 4149  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4047  df-un 4151  df-nul 4279

This theorem is used by:  0un  4345  un00  4356  csbun  4398  disjssun  4420  difun2  4436  difdifdir  4446  disjpr2  4670  prprc1  4722  diftpsn3  4761  symdif0  5044  symdifid  5046  iununi  5058  unidif0  5320  unidif0OLD  5321  relresdm1  6024  difxp1  6155  difxp2  6156  suc0  6440  sucprc  6441  fresaun  6753  fresaunres2  6754  fvun1  6976  fndifnfp  7181  fvunsn  7184  fvsnun1  7187  fvsnun2  7188  fsnunfv  7192  fsnunres  7193  funiunfv  7252  fnsuppeq0  8212  frrlem12  8318  oev2  8534  oarec  8573  undifixp  8965  domss2  9158  unfi  9189  domunfican  9316  kmlem2  10233  kmlem3  10234  kmlem11  10242  dju0en  10257  djuassen  10260  ackbij1lem1  10300  ackbij1lem13  10312  fin1a2lem10  10490  fin1a2lem12  10492  axdc3lem4  10534  ttukeylem6  10595  alephadd  10665  fpwwe2lem12  10730  indconst1  12336  prunioo  13615  fzsuc2  13719  fseq1p1m1  13735  hashgval  14480  hashinf  14482  hashfun  14585  sadid1  16643  lcmfunsnlem  16821  lcmfun  16825  vdwap1  17160  setsres  17361  setsid  17390  mreexexlem3d  17825  mreexdomd  17828  pwmndid  19147  pwmnd  19148  pwssplit1  21339  lspsnat  21428  lsppratlem3  21432  lindsdom  22161  opsrtoslem2  22370  indistopon  23324  indistps  23334  indistps2  23335  restcld  23495  neitr  23503  refun0  23839  filconn  24207  ufildr  24255  restmetu  24894  ovolioo  25894  itgsplitioo  26163  plyeq0  26535  birthdaylem2  27285  lgsquadlem2  27713  noextendseq  28029  nosupbnd2lem1  28077  noinfbnd2lem1  28092  noetasuplem2  28096  noetasuplem3  28097  noetasuplem4  28098  noetainflem2  28100  bday1  28205  lrold  28288  addsrid  28355  negsproplem2  28420  negsproplem6  28424  muls01  28503  mulsrid  28504  mulsproplem2  28508  mulsproplem3  28509  mulsproplem4  28510  mulsproplem12  28518  mulsproplem13  28519  mulsproplem14  28520  onleft  28651  ltonold  28652  oncutlt  28655  oniso  28662  bdayons  28667  onaddscl  28668  onmulscl  28669  n0cut  28725  n0bday  28743  bdayn0p1  28760  0reno  28887  1reno  28888  ex-dif  31029  ex-in  31031  ex-res  31047  difres  33241  imadifxp  33242  ofpreima2  33307  coprprop  33339  padct  33357  difico  33421  tocycf  33724  tocyc01  33725  elrgspnlem4  33852  esplyind  34253  constrextdg2lem  34426  locfinref  34519  sigaclfu2  34799  prsiga  34809  unelldsys  34837  measun  34890  difelcarsg  34988  carsgclctunlem1  34995  carsggect  34996  eulerpartlemt  35049  eulerpartgbij  35050  ballotlemfp1  35170  fineqvac  35840  indispconn  36085  onint1  37329  bj-pr21val  38018  bj-funun  38266  poimirlem3  38634  poimirlem5  38636  poimirlem10  38641  poimirlem15  38646  poimirlem22  38653  poimirlem23  38654  poimirlem28  38659  padd01  40961  padd02  40962  pclfinclN  41100  mapfzcons1  43821  fzsplit1nn0  43858  diophrw  43863  eldioph2lem1  43864  eldioph2lem2  43865  diophren  43913  pwssplit4  44184  mnuprdlem1  45349  dvmptfprodlem  47047  caratheodorylem1  47629  isomenndlem  47633  fzopredsuc  48487  clnbgr0edg  49028  tposrescnv  50085  tposres2  50086  tposres3  50087  parhomssun  50840  aacllem  51107