Theorem unidm 4119

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

Syntax hints:   = wceq 1567   ∈ wcel 2149   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918

This theorem is referenced by:  unundi  4137  unundir  4138  uneqin  4250  difabs  4264  undifabs  4444  dfif5  4509  dfsn2  4607  unisng  4894  dfdm2  6283  unixpid  6286  fun2  6742  resasplit  6749  xpider  8786  pm54.43  9987  dmtrclfv  15055  lefld  18648  symg2bas  19463  gsumzaddlem  19991  pwssplit1  21158  plyun0  26323  nodenselem5  27818  addsproplem6  28133  mulsproplem12  28286  mulsproplem13  28287  mulsproplem14  28288  n0cut  28493  twocut  28582  halfcut  28617  pw2cut2  28621  readdscl  28658  remulscl  28661  wlkp1  29970  cycpmco2f1  33385  carsgsigalem  34650  sseqf  34727  probun  34754  filnetlem3  36780  pibt2  37951  mapfzcons  43339  diophin  43395  pwssplit4  43708  fiuneneq  43811  rclexi  44233  rtrclex  44235  dfrtrcl5  44247  dfrcl2  44292  iunrelexp0  44320  relexpiidm  44322  corclrcl  44325  relexp01min  44331  cotrcltrcl  44343  clsk1indlem3  44661  fiiuncl  45677  fzopredsuc  47950