Theorem unidm 4111

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146   ∪ cun 3904

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911

This theorem is used by:  unundi  4129  unundir  4130  uneqin  4242  difabs  4256  undifabs  4441  dfif5  4506  dfsn2  4604  unisng  4892  dfdm2  6286  unixpid  6289  fun2  6745  resasplit  6752  xpider  8792  pm54.43  10003  dmtrclfv  15081  lefld  18672  symg2bas  19509  gsumzaddlem  20037  pwssplit1  21232  plyun0  26407  nodenselem5  27905  addsproplem6  28220  mulsproplem12  28373  mulsproplem13  28374  mulsproplem14  28375  n0cut  28580  twocut  28669  halfcut  28704  pw2cut2  28708  readdscl  28745  remulscl  28748  wlkp1  30089  cycpmco2f1  33510  carsgsigalem  34772  sseqf  34849  probun  34876  filnetlem3  36950  pibt2  38122  mapfzcons  43507  diophin  43563  pwssplit4  43876  fiuneneq  43979  rclexi  44401  rtrclex  44403  dfrtrcl5  44415  dfrcl2  44460  iunrelexp0  44488  relexpiidm  44490  corclrcl  44493  relexp01min  44499  cotrcltrcl  44511  clsk1indlem3  44829  fiiuncl  45845  fzopredsuc  48121