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

Syntax hints:   = wceq 1570   ∈ wcel 2143   ∪ cun 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910

This theorem is referenced by:  unundi  4129  unundir  4130  uneqin  4242  difabs  4256  undifabs  4439  dfif5  4504  dfsn2  4602  unisng  4890  dfdm2  6282  unixpid  6285  fun2  6741  resasplit  6748  xpider  8782  pm54.43  9983  dmtrclfv  15051  lefld  18643  symg2bas  19458  gsumzaddlem  19986  pwssplit1  21180  plyun0  26354  nodenselem5  27852  addsproplem6  28167  mulsproplem12  28320  mulsproplem13  28321  mulsproplem14  28322  n0cut  28527  twocut  28616  halfcut  28651  pw2cut2  28655  readdscl  28692  remulscl  28695  wlkp1  30029  cycpmco2f1  33444  carsgsigalem  34705  sseqf  34782  probun  34809  filnetlem3  36911  pibt2  38083  mapfzcons  43467  diophin  43523  pwssplit4  43836  fiuneneq  43939  rclexi  44361  rtrclex  44363  dfrtrcl5  44375  dfrcl2  44420  iunrelexp0  44448  relexpiidm  44450  corclrcl  44453  relexp01min  44459  cotrcltrcl  44471  clsk1indlem3  44789  fiiuncl  45805  fzopredsuc  48081