Theorem unidm 4107

Description: Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
unidm	⊢ (𝐴 ∪ 𝐴) = 𝐴

Proof of Theorem unidm

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		oridm 904	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐴) ↔ 𝑥 ∈ 𝐴)
2	1	uneqri 4106	1 ⊢ (𝐴 ∪ 𝐴) = 𝐴

Syntax hints:   = wceq 1541   ∈ wcel 2113   ∪ cun 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904

This theorem is referenced by:  unundi  4126  unundir  4127  uneqin  4239  difabs  4253  undifabs  4428  dfif5  4494  dfsn2  4591  unisng  4879  dfdm2  6237  unixpid  6240  f1imadifssran  6576  fun2  6695  resasplit  6702  xpider  8723  pm54.43  9911  dmtrclfv  14939  lefld  18513  symg2bas  19320  gsumzaddlem  19848  pwssplit1  21009  plyun0  26156  nodenselem5  27654  addsproplem6  27944  mulsproplem12  28096  mulsproplem13  28097  mulsproplem14  28098  n0scut  28294  1p1e2s  28374  twocut  28381  halfcut  28415  pw2cut2  28419  readdscl  28444  remulscl  28447  wlkp1  29702  cycpmco2f1  33155  carsgsigalem  34421  sseqf  34498  probun  34525  filnetlem3  36523  pibt2  37561  mapfzcons  42900  diophin  42956  pwssplit4  43273  fiuneneq  43376  rclexi  43798  rtrclex  43800  dfrtrcl5  43812  dfrcl2  43857  iunrelexp0  43885  relexpiidm  43887  corclrcl  43890  relexp01min  43896  cotrcltrcl  43908  clsk1indlem3  44226  fiiuncl  45252  fzopredsuc  47511