Theorem unidm 4158

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2146   ∪ cun 4151

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-un 4153

This theorem is used by:  unundi  4176  unundir  4177  uneqin  4236  difabs  4250  undifabs  4436  dfif5  4501  dfsn2  4596  unisng  4887  dfdm2  6290  unixpid  6293  fun2  6753  resasplit  6760  xpider  8820  pm54.43  10092  dmtrclfv  15183  lefld  18778  symg2bas  19619  gsumzaddlem  20147  pwssplit1  21346  plyun0  26527  nodenselem5  28057  addsproplem6  28372  mulsproplem12  28525  mulsproplem13  28526  mulsproplem14  28527  n0cut  28732  twocut  28821  halfcut  28856  pw2cut2  28860  readdscl  28897  remulscl  28900  wlkp1  30272  cycpmco2f1  33738  carsgsigalem  35000  sseqf  35077  probun  35104  filnetlem3  37295  pibt2  38480  mapfzcons  43867  diophin  43923  pwssplit4  44231  fiuneneq  44334  rclexi  44755  rtrclex  44757  dfrtrcl5  44769  dfrcl2  44814  iunrelexp0  44842  relexpiidm  44844  corclrcl  44847  relexp01min  44853  cotrcltrcl  44865  clsk1indlem3  45183  fiiuncl  46221  fzopredsuc  48533