Theorem unidm 4087

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

Syntax hints:   = wceq 1547   ∈ wcel 2119   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888

This theorem is referenced by:  unundi  4105  unundir  4106  uneqin  4217  difabs  4231  undifabs  4406  dfif5  4471  dfsn2  4568  unisng  4856  dfdm2  6232  unixpid  6235  f1imadifssran  6571  fun2  6690  resasplit  6697  xpider  8725  pm54.43  9916  dmtrclfv  14971  lefld  18549  symg2bas  19359  gsumzaddlem  19887  pwssplit1  21049  plyun0  26180  nodenselem5  27670  addsproplem6  27984  mulsproplem12  28137  mulsproplem13  28138  mulsproplem14  28139  n0cut  28344  twocut  28433  halfcut  28468  pw2cut2  28472  readdscl  28509  remulscl  28512  wlkp1  29766  cycpmco2f1  33205  carsgsigalem  34499  sseqf  34576  probun  34603  filnetlem3  36608  pibt2  37779  mapfzcons  43165  diophin  43221  pwssplit4  43534  fiuneneq  43637  rclexi  44059  rtrclex  44061  dfrtrcl5  44073  dfrcl2  44118  iunrelexp0  44146  relexpiidm  44148  corclrcl  44151  relexp01min  44157  cotrcltrcl  44169  clsk1indlem3  44487  fiiuncl  45513  fzopredsuc  47787