Theorem unidm 4109

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

Syntax hints:   = wceq 1541   ∈ wcel 2113   ∪ cun 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906

This theorem is referenced by:  unundi  4128  unundir  4129  uneqin  4241  difabs  4255  undifabs  4430  dfif5  4496  dfsn2  4593  unisng  4881  dfdm2  6239  unixpid  6242  f1imadifssran  6578  fun2  6697  resasplit  6704  xpider  8725  pm54.43  9913  dmtrclfv  14941  lefld  18515  symg2bas  19322  gsumzaddlem  19850  pwssplit1  21011  plyun0  26158  nodenselem5  27656  addsproplem6  27970  mulsproplem12  28123  mulsproplem13  28124  mulsproplem14  28125  n0cut  28330  twocut  28419  halfcut  28454  pw2cut2  28458  readdscl  28495  remulscl  28498  wlkp1  29753  cycpmco2f1  33206  carsgsigalem  34472  sseqf  34549  probun  34576  filnetlem3  36574  pibt2  37622  mapfzcons  42958  diophin  43014  pwssplit4  43331  fiuneneq  43434  rclexi  43856  rtrclex  43858  dfrtrcl5  43870  dfrcl2  43915  iunrelexp0  43943  relexpiidm  43945  corclrcl  43948  relexp01min  43954  cotrcltrcl  43966  clsk1indlem3  44284  fiiuncl  45310  fzopredsuc  47569