Theorem unidm 4098

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

Syntax hints:   = wceq 1542   ∈ wcel 2114   ∪ cun 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895

This theorem is referenced by:  unundi  4117  unundir  4118  uneqin  4230  difabs  4244  undifabs  4419  dfif5  4484  dfsn2  4581  unisng  4869  dfdm2  6240  unixpid  6243  f1imadifssran  6579  fun2  6698  resasplit  6705  xpider  8729  pm54.43  9919  dmtrclfv  14974  lefld  18552  symg2bas  19362  gsumzaddlem  19890  pwssplit1  21049  plyun0  26175  nodenselem5  27669  addsproplem6  27983  mulsproplem12  28136  mulsproplem13  28137  mulsproplem14  28138  n0cut  28343  twocut  28432  halfcut  28467  pw2cut2  28471  readdscl  28508  remulscl  28511  wlkp1  29766  cycpmco2f1  33203  carsgsigalem  34478  sseqf  34555  probun  34582  filnetlem3  36581  pibt2  37750  mapfzcons  43165  diophin  43221  pwssplit4  43538  fiuneneq  43641  rclexi  44063  rtrclex  44065  dfrtrcl5  44077  dfrcl2  44122  iunrelexp0  44150  relexpiidm  44152  corclrcl  44155  relexp01min  44161  cotrcltrcl  44173  clsk1indlem3  44491  fiiuncl  45517  fzopredsuc  47787