Theorem unidm 4108

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

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

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 3438  df-un 3908

This theorem is referenced by:  unundi  4127  unundir  4128  uneqin  4240  difabs  4254  undifabs  4429  dfif5  4493  dfsn2  4590  unisng  4876  dfdm2  6229  unixpid  6232  f1imadifssran  6568  fun2  6687  resasplit  6694  xpider  8715  pm54.43  9897  dmtrclfv  14925  lefld  18498  symg2bas  19272  gsumzaddlem  19800  pwssplit1  20963  plyun0  26100  nodenselem5  27598  addsproplem6  27886  mulsproplem12  28035  mulsproplem13  28036  mulsproplem14  28037  n0scut  28231  1p1e2s  28308  twocut  28315  halfcut  28346  readdscl  28368  remulscl  28371  wlkp1  29625  cycpmco2f1  33066  carsgsigalem  34283  sseqf  34360  probun  34387  filnetlem3  36358  pibt2  37395  mapfzcons  42693  diophin  42749  pwssplit4  43066  fiuneneq  43169  rclexi  43592  rtrclex  43594  dfrtrcl5  43606  dfrcl2  43651  iunrelexp0  43679  relexpiidm  43681  corclrcl  43684  relexp01min  43690  cotrcltrcl  43702  clsk1indlem3  44020  fiiuncl  45047  fzopredsuc  47311