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  18527  symg2bas  19299  gsumzaddlem  19827  pwssplit1  20942  plyun0  26078  nodenselem5  27576  addsproplem6  27857  mulsproplem12  28006  mulsproplem13  28007  mulsproplem14  28008  n0scut  28202  1p1e2s  28278  twocut  28285  halfcut  28309  readdscl  28326  remulscl  28329  wlkp1  29583  cycpmco2f1  33054  carsgsigalem  34279  sseqf  34356  probun  34383  filnetlem3  36341  pibt2  37378  mapfzcons  42677  diophin  42733  pwssplit4  43051  fiuneneq  43154  rclexi  43577  rtrclex  43579  dfrtrcl5  43591  dfrcl2  43636  iunrelexp0  43664  relexpiidm  43666  corclrcl  43669  relexp01min  43675  cotrcltrcl  43687  clsk1indlem3  44005  fiiuncl  45032  fzopredsuc  47297