Theorem unidm 4120

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

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

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 3449  df-un 3919

This theorem is referenced by:  unundi  4139  unundir  4140  uneqin  4252  difabs  4266  undifabs  4441  dfif5  4505  dfsn2  4602  unisng  4889  dfdm2  6254  unixpid  6257  f1imadifssran  6602  fun2  6723  resasplit  6730  xpider  8761  pm54.43  9954  dmtrclfv  14984  lefld  18551  symg2bas  19323  gsumzaddlem  19851  pwssplit1  20966  plyun0  26102  nodenselem5  27600  addsproplem6  27881  mulsproplem12  28030  mulsproplem13  28031  mulsproplem14  28032  n0scut  28226  1p1e2s  28302  twocut  28309  halfcut  28333  readdscl  28350  remulscl  28353  wlkp1  29609  cycpmco2f1  33081  carsgsigalem  34306  sseqf  34383  probun  34410  filnetlem3  36368  pibt2  37405  mapfzcons  42704  diophin  42760  pwssplit4  43078  fiuneneq  43181  rclexi  43604  rtrclex  43606  dfrtrcl5  43618  dfrcl2  43663  iunrelexp0  43691  relexpiidm  43693  corclrcl  43696  relexp01min  43702  cotrcltrcl  43714  clsk1indlem3  44032  fiiuncl  45059  fzopredsuc  47324