Theorem unidm 4110

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 915	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐴) ↔ 𝑥 ∈ 𝐴)
2	1	uneqri 4109	1 ⊢ (𝐴 ∪ 𝐴) = 𝐴

Syntax hints:   = wceq 1560   ∈ wcel 2142   ∪ cun 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909

This theorem is referenced by:  unundi  4128  unundir  4129  uneqin  4241  difabs  4255  undifabs  4432  dfif5  4497  dfsn2  4595  unisng  4883  dfdm2  6268  unixpid  6271  f1imadifssran  6607  fun2  6727  resasplit  6734  xpider  8770  pm54.43  9959  dmtrclfv  15031  lefld  18624  symg2bas  19433  gsumzaddlem  19961  pwssplit1  21126  plyun0  26257  nodenselem5  27752  addsproplem6  28067  mulsproplem12  28220  mulsproplem13  28221  mulsproplem14  28222  n0cut  28427  twocut  28516  halfcut  28551  pw2cut2  28555  readdscl  28592  remulscl  28595  wlkp1  29880  cycpmco2f1  33304  carsgsigalem  34612  sseqf  34689  probun  34716  filnetlem3  36740  pibt2  37911  mapfzcons  43297  diophin  43353  pwssplit4  43666  fiuneneq  43769  rclexi  44191  rtrclex  44193  dfrtrcl5  44205  dfrcl2  44250  iunrelexp0  44278  relexpiidm  44280  corclrcl  44283  relexp01min  44289  cotrcltrcl  44301  clsk1indlem3  44619  fiiuncl  45645  fzopredsuc  47918