Theorem un0 3967

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 3919	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfi 422	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 214	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 3755	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 383   = wceq 1483   ∈ wcel 1990   ∪ cun 3572  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-un 3579  df-nul 3916

This theorem is referenced by:  csbun  4009  un00  4011  disjssun  4036  difun2  4048  difdifdir  4056  disjpr2  4248  disjpr2OLD  4249  prprc1  4300  diftpsn3  4332  diftpsn3OLD  4333  sspr  4366  sstp  4367  symdif0  4597  symdifv  4598  symdifid  4599  iunxdif3  4606  iununi  4610  unidif0  4838  difxp1  5559  difxp2  5560  suc0  5799  sucprc  5800  fresaun  6075  fresaunres2  6076  fvssunirn  6217  fvun1  6269  fndifnfp  6442  fvunsn  6445  fvsnun1  6448  fvsnun2  6449  fsnunfv  6453  fsnunres  6454  funiunfv  6506  fnsuppeq0  7323  wfrlem14  7428  oev2  7603  oarec  7642  undifixp  7944  domss2  8119  domunfican  8233  kmlem2  8973  kmlem3  8974  kmlem11  8982  cda0en  9001  cdaassen  9004  ackbij1lem1  9042  ackbij1lem13  9054  fin1a2lem10  9231  fin1a2lem12  9233  axdc3lem4  9275  ttukeylem6  9336  alephadd  9399  fpwwe2lem13  9464  prunioo  12301  fzsuc2  12398  fseq1p1m1  12414  hashgval  13120  hashinf  13122  hashfun  13224  sadid1  15190  lcmfunsnlem  15354  lcmfun  15358  vdwap1  15681  setsres  15901  setsid  15914  mreexexlem3d  16306  mreexdomd  16310  pwssplit1  19059  lspsnat  19145  lsppratlem3  19149  opsrtoslem2  19485  indistopon  20805  indistps  20815  indistps2  20816  restcld  20976  neitr  20984  refun0  21318  filconn  21687  ufildr  21735  restmetu  22375  ovolioo  23336  itgsplitioo  23604  plyeq0  23967  birthdaylem2  24679  lgsquadlem2  25106  ex-dif  27280  ex-in  27282  ex-res  27298  difres  29413  imadifxp  29414  funresdm1  29416  ofpreima2  29466  padct  29497  difico  29545  locfinref  29908  sigaclfu2  30184  prsiga  30194  unelldsys  30221  measun  30274  difelcarsg  30372  carsgclctunlem1  30379  carsggect  30380  eulerpartlemt  30433  eulerpartgbij  30434  ballotlemfp1  30553  indispconn  31216  noextendseq  31820  nosupbnd2lem1  31861  noetalem2  31864  noetalem3  31865  onint1  32448  bj-pr21val  33001  bj-pr22val  33007  lindsdom  33403  poimirlem3  33412  poimirlem5  33414  poimirlem10  33419  poimirlem15  33424  poimirlem22  33431  poimirlem23  33432  poimirlem28  33437  padd01  35097  padd02  35098  pclfinclN  35236  mapfzcons1  37280  fzsplit1nn0  37317  diophrw  37322  eldioph2lem1  37323  eldioph2lem2  37324  diophren  37377  pwssplit4  37659  0un  39215  dvmptfprodlem  40159  prsal  40538  caratheodorylem1  40740  isomenndlem  40744  fzopredsuc  41333  aacllem  42547