Theorem unidm 4137

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

Syntax hints:   = wceq 1539   ∈ wcel 2107   ∪ cun 3929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465  df-un 3936

This theorem is referenced by:  unundi  4156  unundir  4157  uneqin  4269  difabs  4283  undifabs  4458  dfif5  4522  dfsn2  4619  unisng  4905  dfdm2  6281  unixpid  6284  f1imadifssran  6632  fun2  6751  resasplit  6758  xpider  8810  pm54.43  10023  dmtrclfv  15040  lefld  18607  symg2bas  19379  gsumzaddlem  19908  pwssplit1  21027  plyun0  26173  nodenselem5  27670  addsproplem6  27944  mulsproplem12  28090  mulsproplem13  28091  mulsproplem14  28092  n0scut  28275  1p1e2s  28337  nohalf  28344  halfcut  28353  readdscl  28368  remulscl  28371  wlkp1  29628  cycpmco2f1  33088  carsgsigalem  34292  sseqf  34369  probun  34396  filnetlem3  36356  pibt2  37393  metakunt21  42201  metakunt22  42202  metakunt24  42204  mapfzcons  42705  diophin  42761  pwssplit4  43079  fiuneneq  43182  rclexi  43605  rtrclex  43607  dfrtrcl5  43619  dfrcl2  43664  iunrelexp0  43692  relexpiidm  43694  corclrcl  43697  relexp01min  43703  cotrcltrcl  43715  clsk1indlem3  44033  fiiuncl  45042  fzopredsuc  47308