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

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908

This theorem is referenced by:  unundi  4130  unundir  4131  uneqin  4243  difabs  4257  undifabs  4432  dfif5  4498  dfsn2  4595  unisng  4883  dfdm2  6247  unixpid  6250  f1imadifssran  6586  fun2  6705  resasplit  6712  xpider  8737  pm54.43  9925  dmtrclfv  14953  lefld  18527  symg2bas  19334  gsumzaddlem  19862  pwssplit1  21023  plyun0  26170  nodenselem5  27668  addsproplem6  27982  mulsproplem12  28135  mulsproplem13  28136  mulsproplem14  28137  n0cut  28342  twocut  28431  halfcut  28466  pw2cut2  28470  readdscl  28507  remulscl  28510  wlkp1  29765  cycpmco2f1  33218  carsgsigalem  34493  sseqf  34570  probun  34597  filnetlem3  36596  pibt2  37672  mapfzcons  43073  diophin  43129  pwssplit4  43446  fiuneneq  43549  rclexi  43971  rtrclex  43973  dfrtrcl5  43985  dfrcl2  44030  iunrelexp0  44058  relexpiidm  44060  corclrcl  44063  relexp01min  44069  cotrcltrcl  44081  clsk1indlem3  44399  fiiuncl  45425  fzopredsuc  47683