Theorem unidm 4104

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 4103	1 ⊢ (𝐴 ∪ 𝐴) = 𝐴

Syntax hints:   = wceq 1541   ∈ wcel 2111   ∪ cun 3895

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902

This theorem is referenced by:  unundi  4123  unundir  4124  uneqin  4236  difabs  4250  undifabs  4425  dfif5  4489  dfsn2  4586  unisng  4874  dfdm2  6228  unixpid  6231  f1imadifssran  6567  fun2  6686  resasplit  6693  xpider  8712  pm54.43  9894  dmtrclfv  14925  lefld  18498  symg2bas  19305  gsumzaddlem  19833  pwssplit1  20993  plyun0  26129  nodenselem5  27627  addsproplem6  27917  mulsproplem12  28066  mulsproplem13  28067  mulsproplem14  28068  n0scut  28262  1p1e2s  28339  twocut  28346  halfcut  28378  pw2cut2  28382  readdscl  28401  remulscl  28404  wlkp1  29658  cycpmco2f1  33093  carsgsigalem  34328  sseqf  34405  probun  34432  filnetlem3  36424  pibt2  37461  mapfzcons  42819  diophin  42875  pwssplit4  43192  fiuneneq  43295  rclexi  43718  rtrclex  43720  dfrtrcl5  43732  dfrcl2  43777  iunrelexp0  43805  relexpiidm  43807  corclrcl  43810  relexp01min  43816  cotrcltrcl  43828  clsk1indlem3  44146  fiiuncl  45172  fzopredsuc  47433