Theorem unidm 4180

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 903	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐴) ↔ 𝑥 ∈ 𝐴)
2	1	uneqri 4179	1 ⊢ (𝐴 ∪ 𝐴) = 𝐴

Syntax hints:   = wceq 1537   ∈ wcel 2108   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981

This theorem is referenced by:  unundi  4199  unundir  4200  uneqin  4308  difabs  4322  undifabs  4501  dfif5  4564  dfsn2  4661  unisng  4949  dfdm2  6312  unixpid  6315  fun2  6784  resasplit  6791  xpider  8846  pm54.43  10070  dmtrclfv  15067  lefld  18662  symg2bas  19434  gsumzaddlem  19963  pwssplit1  21081  plyun0  26256  nodenselem5  27751  addsproplem6  28025  mulsproplem12  28171  mulsproplem13  28172  mulsproplem14  28173  n0scut  28356  1p1e2s  28418  nohalf  28425  halfcut  28434  readdscl  28449  remulscl  28452  wlkp1  29717  cycpmco2f1  33117  carsgsigalem  34280  sseqf  34357  probun  34384  filnetlem3  36346  pibt2  37383  metakunt21  42182  metakunt22  42183  metakunt24  42185  mapfzcons  42672  diophin  42728  pwssplit4  43046  fiuneneq  43153  rclexi  43577  rtrclex  43579  dfrtrcl5  43591  dfrcl2  43636  iunrelexp0  43664  relexpiidm  43666  corclrcl  43669  relexp01min  43675  cotrcltrcl  43687  clsk1indlem3  44005  fiiuncl  44967  fzopredsuc  47238