Theorem unidm 4097

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

Syntax hints:   = wceq 1542   ∈ wcel 2114   ∪ cun 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894

This theorem is referenced by:  unundi  4116  unundir  4117  uneqin  4229  difabs  4243  undifabs  4418  dfif5  4483  dfsn2  4580  unisng  4868  dfdm2  6245  unixpid  6248  f1imadifssran  6584  fun2  6703  resasplit  6710  xpider  8735  pm54.43  9925  dmtrclfv  14980  lefld  18558  symg2bas  19368  gsumzaddlem  19896  pwssplit1  21054  plyun0  26162  nodenselem5  27652  addsproplem6  27966  mulsproplem12  28119  mulsproplem13  28120  mulsproplem14  28121  n0cut  28326  twocut  28415  halfcut  28450  pw2cut2  28454  readdscl  28491  remulscl  28494  wlkp1  29748  cycpmco2f1  33185  carsgsigalem  34459  sseqf  34536  probun  34563  filnetlem3  36562  pibt2  37733  mapfzcons  43148  diophin  43204  pwssplit4  43517  fiuneneq  43620  rclexi  44042  rtrclex  44044  dfrtrcl5  44056  dfrcl2  44101  iunrelexp0  44129  relexpiidm  44131  corclrcl  44134  relexp01min  44140  cotrcltrcl  44152  clsk1indlem3  44470  fiiuncl  45496  fzopredsuc  47772