Theorem unidm 4123

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

Syntax hints:   = wceq 1540   ∈ wcel 2109   ∪ cun 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922

This theorem is referenced by:  unundi  4142  unundir  4143  uneqin  4255  difabs  4269  undifabs  4444  dfif5  4508  dfsn2  4605  unisng  4892  dfdm2  6257  unixpid  6260  f1imadifssran  6605  fun2  6726  resasplit  6733  xpider  8764  pm54.43  9961  dmtrclfv  14991  lefld  18558  symg2bas  19330  gsumzaddlem  19858  pwssplit1  20973  plyun0  26109  nodenselem5  27607  addsproplem6  27888  mulsproplem12  28037  mulsproplem13  28038  mulsproplem14  28039  n0scut  28233  1p1e2s  28309  twocut  28316  halfcut  28340  readdscl  28357  remulscl  28360  wlkp1  29616  cycpmco2f1  33088  carsgsigalem  34313  sseqf  34390  probun  34417  filnetlem3  36375  pibt2  37412  mapfzcons  42711  diophin  42767  pwssplit4  43085  fiuneneq  43188  rclexi  43611  rtrclex  43613  dfrtrcl5  43625  dfrcl2  43670  iunrelexp0  43698  relexpiidm  43700  corclrcl  43703  relexp01min  43709  cotrcltrcl  43721  clsk1indlem3  44039  fiiuncl  45066  fzopredsuc  47328