Theorem unidm 4157

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

Syntax hints:   = wceq 1540   ∈ wcel 2108   ∪ cun 3949

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956

This theorem is referenced by:  unundi  4176  unundir  4177  uneqin  4289  difabs  4303  undifabs  4478  dfif5  4542  dfsn2  4639  unisng  4925  dfdm2  6301  unixpid  6304  f1imadifssran  6652  fun2  6771  resasplit  6778  xpider  8828  pm54.43  10041  dmtrclfv  15057  lefld  18637  symg2bas  19410  gsumzaddlem  19939  pwssplit1  21058  plyun0  26236  nodenselem5  27733  addsproplem6  28007  mulsproplem12  28153  mulsproplem13  28154  mulsproplem14  28155  n0scut  28338  1p1e2s  28400  nohalf  28407  halfcut  28416  readdscl  28431  remulscl  28434  wlkp1  29699  cycpmco2f1  33144  carsgsigalem  34317  sseqf  34394  probun  34421  filnetlem3  36381  pibt2  37418  metakunt21  42226  metakunt22  42227  metakunt24  42229  mapfzcons  42727  diophin  42783  pwssplit4  43101  fiuneneq  43204  rclexi  43628  rtrclex  43630  dfrtrcl5  43642  dfrcl2  43687  iunrelexp0  43715  relexpiidm  43717  corclrcl  43720  relexp01min  43726  cotrcltrcl  43738  clsk1indlem3  44056  fiiuncl  45070  fzopredsuc  47335