Theorem unidm 4132

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

Syntax hints:   = wceq 1540   ∈ wcel 2108   ∪ cun 3924

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931

This theorem is referenced by:  unundi  4151  unundir  4152  uneqin  4264  difabs  4278  undifabs  4453  dfif5  4517  dfsn2  4614  unisng  4901  dfdm2  6270  unixpid  6273  f1imadifssran  6622  fun2  6741  resasplit  6748  xpider  8802  pm54.43  10015  dmtrclfv  15037  lefld  18602  symg2bas  19374  gsumzaddlem  19902  pwssplit1  21017  plyun0  26154  nodenselem5  27652  addsproplem6  27933  mulsproplem12  28082  mulsproplem13  28083  mulsproplem14  28084  n0scut  28278  1p1e2s  28354  twocut  28361  halfcut  28385  readdscl  28402  remulscl  28405  wlkp1  29661  cycpmco2f1  33135  carsgsigalem  34347  sseqf  34424  probun  34451  filnetlem3  36398  pibt2  37435  metakunt21  42238  metakunt22  42239  metakunt24  42241  mapfzcons  42739  diophin  42795  pwssplit4  43113  fiuneneq  43216  rclexi  43639  rtrclex  43641  dfrtrcl5  43653  dfrcl2  43698  iunrelexp0  43726  relexpiidm  43728  corclrcl  43731  relexp01min  43737  cotrcltrcl  43749  clsk1indlem3  44067  fiiuncl  45089  fzopredsuc  47352