Theorem unidm 4153

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

Syntax hints:   = wceq 1539   ∈ wcel 2104   ∪ cun 3947

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3954

This theorem is referenced by:  unundi  4171  unundir  4172  uneqin  4279  difabs  4294  undifabs  4478  dfif5  4545  dfsn2  4642  unisng  4930  dfdm2  6281  unixpid  6284  fun2  6755  resasplit  6762  xpider  8786  pm54.43  10000  dmtrclfv  14971  lefld  18551  symg2bas  19303  gsumzaddlem  19832  pwssplit1  20816  plyun0  25945  nodenselem5  27425  addsproplem6  27694  mulsproplem12  27820  mulsproplem13  27821  mulsproplem14  27822  n0scut  27941  wlkp1  29203  cycpmco2f1  32551  carsgsigalem  33610  sseqf  33687  probun  33714  filnetlem3  35570  pibt2  36603  metakunt21  41313  metakunt22  41314  metakunt24  41316  mapfzcons  41758  diophin  41814  pwssplit4  42135  fiuneneq  42243  rclexi  42670  rtrclex  42672  dfrtrcl5  42684  dfrcl2  42729  iunrelexp0  42757  relexpiidm  42759  corclrcl  42762  relexp01min  42768  cotrcltrcl  42780  clsk1indlem3  43098  fiiuncl  44055  fzopredsuc  46331