Theorem un0 4191

Description: The union of a class with the empty set is itself. 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 4147	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfi 969	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 216	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 3981	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 880   = wceq 1658   ∈ wcel 2166   ∪ cun 3795  ∅c0 4143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-v 3415  df-dif 3800  df-un 3802  df-nul 4144

This theorem is referenced by:  csbun  4233  un00  4235  disjssun  4258  difun2  4270  difdifdir  4278  disjpr2  4466  prprc1  4517  diftpsn3  4550  sspr  4581  sstp  4582  symdif0  4816  symdifv  4817  symdifid  4818  iunxdif3  4826  iununi  4830  unidif0  5059  difxp1  5799  difxp2  5800  suc0  6036  sucprc  6037  fresaun  6311  fresaunres2  6312  fvssunirn  6461  fvun1  6515  fndifnfp  6693  fvunsn  6696  fvsnun1  6701  fvsnun2  6702  fvsnun1OLD  6703  fvsnun2OLD  6704  fsnunfv  6708  fsnunres  6709  funiunfv  6760  fnsuppeq0  7587  wfrlem14  7693  oev2  7869  oarec  7908  undifixp  8210  domss2  8387  domunfican  8501  kmlem2  9287  kmlem3  9288  kmlem11  9296  cda0en  9315  cdaassen  9318  ackbij1lem1  9356  ackbij1lem13  9368  fin1a2lem10  9545  fin1a2lem12  9547  axdc3lem4  9589  ttukeylem6  9650  alephadd  9713  fpwwe2lem13  9778  prunioo  12593  fzsuc2  12691  fseq1p1m1  12707  hashgval  13412  hashinf  13414  hashfun  13512  sadid1  15562  lcmfunsnlem  15726  lcmfun  15730  vdwap1  16051  setsres  16263  setsid  16276  mreexexlem3d  16658  mreexdomd  16661  pwssplit1  19417  lspsnat  19504  lsppratlem3  19509  opsrtoslem2  19844  indistopon  21175  indistps  21185  indistps2  21186  restcld  21346  neitr  21354  refun0  21688  filconn  22056  ufildr  22104  restmetu  22744  ovolioo  23733  itgsplitioo  24002  plyeq0  24365  birthdaylem2  25091  lgsquadlem2  25518  ex-dif  27837  ex-in  27839  ex-res  27855  difres  29959  imadifxp  29960  funresdm1  29962  ofpreima2  30014  padct  30044  difico  30091  locfinref  30452  sigaclfu2  30728  prsiga  30738  unelldsys  30765  measun  30818  difelcarsg  30916  carsgclctunlem1  30923  carsggect  30924  eulerpartlemt  30977  eulerpartgbij  30978  ballotlemfp1  31098  indispconn  31761  noextendseq  32358  nosupbnd2lem1  32399  noetalem2  32402  noetalem3  32403  onint1  32980  bj-pr21val  33522  bj-pr22val  33528  bj-funun  33678  lindsdom  33946  poimirlem3  33955  poimirlem5  33957  poimirlem10  33962  poimirlem15  33967  poimirlem22  33974  poimirlem23  33975  poimirlem28  33980  padd01  35885  padd02  35886  pclfinclN  36024  mapfzcons1  38123  fzsplit1nn0  38160  diophrw  38165  eldioph2lem1  38166  eldioph2lem2  38167  diophren  38220  pwssplit4  38501  0un  40031  dvmptfprodlem  40953  prsal  41328  caratheodorylem1  41533  isomenndlem  41537  fzopredsuc  42220  aacllem  43442