Theorem unidm 4166

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

Syntax hints:   = wceq 1536   ∈ wcel 2105   ∪ cun 3960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967

This theorem is referenced by:  unundi  4185  unundir  4186  uneqin  4294  difabs  4308  undifabs  4483  dfif5  4546  dfsn2  4643  unisng  4929  dfdm2  6302  unixpid  6305  fun2  6771  resasplit  6778  xpider  8826  pm54.43  10038  dmtrclfv  15053  lefld  18649  symg2bas  19424  gsumzaddlem  19953  pwssplit1  21075  plyun0  26250  nodenselem5  27747  addsproplem6  28021  mulsproplem12  28167  mulsproplem13  28168  mulsproplem14  28169  n0scut  28352  1p1e2s  28414  nohalf  28421  halfcut  28430  readdscl  28445  remulscl  28448  wlkp1  29713  cycpmco2f1  33126  carsgsigalem  34296  sseqf  34373  probun  34400  filnetlem3  36362  pibt2  37399  metakunt21  42206  metakunt22  42207  metakunt24  42209  mapfzcons  42703  diophin  42759  pwssplit4  43077  fiuneneq  43180  rclexi  43604  rtrclex  43606  dfrtrcl5  43618  dfrcl2  43663  iunrelexp0  43691  relexpiidm  43693  corclrcl  43696  relexp01min  43702  cotrcltrcl  43714  clsk1indlem3  44032  fiiuncl  45004  fzopredsuc  47272