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  6237  unixpid  6240  f1imadifssran  6576  fun2  6695  resasplit  6702  xpider  8726  pm54.43  9914  dmtrclfv  14969  lefld  18547  symg2bas  19357  gsumzaddlem  19885  pwssplit1  21044  plyun0  26170  nodenselem5  27664  addsproplem6  27978  mulsproplem12  28131  mulsproplem13  28132  mulsproplem14  28133  n0cut  28338  twocut  28427  halfcut  28462  pw2cut2  28466  readdscl  28503  remulscl  28506  wlkp1  29761  cycpmco2f1  33198  carsgsigalem  34473  sseqf  34550  probun  34577  filnetlem3  36576  pibt2  37737  mapfzcons  43152  diophin  43208  pwssplit4  43525  fiuneneq  43628  rclexi  44050  rtrclex  44052  dfrtrcl5  44064  dfrcl2  44109  iunrelexp0  44137  relexpiidm  44139  corclrcl  44142  relexp01min  44148  cotrcltrcl  44160  clsk1indlem3  44478  fiiuncl  45504  fzopredsuc  47774