Theorem unidm 4079

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

Syntax hints:   = wceq 1538   ∈ wcel 2111   ∪ cun 3879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886

This theorem is referenced by:  unundi  4097  unundir  4098  uneqin  4205  difabs  4218  undifabs  4384  dfif5  4441  dfsn2  4538  unisng  4819  dfdm2  6100  unixpid  6103  fun2  6515  resasplit  6522  xpider  8351  pm54.43  9414  dmtrclfv  14369  lefld  17828  symg2bas  18513  gsumzaddlem  19034  pwssplit1  19824  plyun0  24794  wlkp1  27471  cycpmco2f1  30816  carsgsigalem  31683  sseqf  31760  probun  31787  nodenselem5  33305  filnetlem3  33841  pibt2  34834  metakunt21  39370  metakunt22  39371  metakunt24  39373  mapfzcons  39657  diophin  39713  pwssplit4  40033  fiuneneq  40141  rclexi  40315  rtrclex  40317  dfrtrcl5  40329  dfrcl2  40375  iunrelexp0  40403  relexpiidm  40405  corclrcl  40408  relexp01min  40414  cotrcltrcl  40426  clsk1indlem3  40746  fiiuncl  41699  fzopredsuc  43880