Theorem unidm 4019

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

Syntax hints:   = wceq 1508   ∈ wcel 2051   ∪ cun 3829

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-v 3419  df-un 3836

This theorem is referenced by:  unundi  4037  unundir  4038  uneqin  4145  difabs  4158  undifabs  4312  dfif5  4369  dfsn2  4457  unisng  4732  dfdm2  5975  unixpid  5978  fun2  6375  resasplit  6382  xpider  8174  pm54.43  9229  dmtrclfv  14245  lefld  17706  symg2bas  18299  gsumzaddlem  18806  pwssplit1  19565  plyun0  24505  wlkp1  27184  carsgsigalem  31250  sseqf  31328  probun  31355  nodenselem5  32753  filnetlem3  33289  pibt2  34179  mapfzcons  38749  diophin  38806  pwssplit4  39126  fiuneneq  39234  rclexi  39379  rtrclex  39381  dfrtrcl5  39393  dfrcl2  39423  iunrelexp0  39451  relexpiidm  39453  corclrcl  39456  relexp01min  39462  cotrcltrcl  39474  clsk1indlem3  39797  fiiuncl  40786  fzopredsuc  42964