Theorem unidm 4104

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145   ∪ cun 3897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904

This theorem is used by:  unundi  4122  unundir  4123  uneqin  4235  difabs  4249  undifabs  4434  dfif5  4499  dfsn2  4597  unisng  4885  dfdm2  6279  unixpid  6282  fun2  6739  resasplit  6746  xpider  8791  pm54.43  10009  dmtrclfv  15094  lefld  18683  symg2bas  19523  gsumzaddlem  20051  pwssplit1  21246  plyun0  26425  nodenselem5  27927  addsproplem6  28242  mulsproplem12  28395  mulsproplem13  28396  mulsproplem14  28397  n0cut  28602  twocut  28691  halfcut  28726  pw2cut2  28730  readdscl  28767  remulscl  28770  wlkp1  30142  cycpmco2f1  33567  carsgsigalem  34829  sseqf  34906  probun  34933  filnetlem3  37002  pibt2  38174  mapfzcons  43564  diophin  43620  pwssplit4  43933  fiuneneq  44036  rclexi  44458  rtrclex  44460  dfrtrcl5  44472  dfrcl2  44517  iunrelexp0  44545  relexpiidm  44547  corclrcl  44550  relexp01min  44556  cotrcltrcl  44568  clsk1indlem3  44886  fiiuncl  45902  fzopredsuc  48215