Theorem unidm 4116

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

Syntax hints:   = wceq 1540   ∈ wcel 2109   ∪ cun 3909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916

This theorem is referenced by:  unundi  4135  unundir  4136  uneqin  4248  difabs  4262  undifabs  4437  dfif5  4501  dfsn2  4598  unisng  4885  dfdm2  6242  unixpid  6245  f1imadifssran  6586  fun2  6705  resasplit  6712  xpider  8738  pm54.43  9930  dmtrclfv  14960  lefld  18533  symg2bas  19307  gsumzaddlem  19835  pwssplit1  20998  plyun0  26135  nodenselem5  27633  addsproplem6  27921  mulsproplem12  28070  mulsproplem13  28071  mulsproplem14  28072  n0scut  28266  1p1e2s  28343  twocut  28350  halfcut  28381  readdscl  28403  remulscl  28406  wlkp1  29660  cycpmco2f1  33096  carsgsigalem  34299  sseqf  34376  probun  34403  filnetlem3  36361  pibt2  37398  mapfzcons  42697  diophin  42753  pwssplit4  43071  fiuneneq  43174  rclexi  43597  rtrclex  43599  dfrtrcl5  43611  dfrcl2  43656  iunrelexp0  43684  relexpiidm  43686  corclrcl  43689  relexp01min  43695  cotrcltrcl  43707  clsk1indlem3  44025  fiiuncl  45052  fzopredsuc  47317