Theorem unidm 4104

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145   ∪ cun 3897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904

This theorem is used by:  unundi  4122  unundir  4123  uneqin  4235  difabs  4249  undifabs  4434  dfif5  4499  dfsn2  4597  unisng  4885  dfdm2  6284  unixpid  6287  fun2  6745  resasplit  6752  xpider  8809  pm54.43  10082  dmtrclfv  15171  lefld  18766  symg2bas  19607  gsumzaddlem  20135  pwssplit1  21334  plyun0  26515  nodenselem5  28045  addsproplem6  28360  mulsproplem12  28513  mulsproplem13  28514  mulsproplem14  28515  n0cut  28720  twocut  28809  halfcut  28844  pw2cut2  28848  readdscl  28885  remulscl  28888  wlkp1  30260  cycpmco2f1  33685  carsgsigalem  34947  sseqf  35024  probun  35051  filnetlem3  37168  pibt2  38340  mapfzcons  43726  diophin  43782  pwssplit4  44090  fiuneneq  44193  rclexi  44614  rtrclex  44616  dfrtrcl5  44628  dfrcl2  44673  iunrelexp0  44701  relexpiidm  44703  corclrcl  44706  relexp01min  44712  cotrcltrcl  44724  clsk1indlem3  45042  fiiuncl  46081  fzopredsuc  48393