Theorem unidm 4159

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147   ∪ cun 4152

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154

This theorem is used by:  unundi  4177  unundir  4178  uneqin  4237  difabs  4251  undifabs  4437  dfif5  4502  dfsn2  4597  unisng  4890  dfdm2  6308  unixpid  6311  fun2  6775  resasplit  6782  xpider  8847  pm54.43  10121  dmtrclfv  15214  lefld  18816  symg2bas  19658  gsumzaddlem  20186  pwssplit1  21385  plyun0  26570  nodenselem5  28102  addsproplem6  28417  mulsproplem12  28570  mulsproplem13  28571  mulsproplem14  28572  n0cut  28777  twocut  28866  halfcut  28901  pw2cut2  28905  readdscl  28942  remulscl  28945  wlkp1  30317  cycpmco2f1  33784  carsgsigalem  35058  sseqf  35135  probun  35162  filnetlem3  37383  pibt2  38608  mapfzcons  43993  diophin  44049  pwssplit4  44357  fiuneneq  44455  rclexi  44876  rtrclex  44878  dfrtrcl5  44890  dfrcl2  44935  iunrelexp0  44963  relexpiidm  44965  corclrcl  44968  relexp01min  44974  cotrcltrcl  44986  clsk1indlem3  45304  fiiuncl  46356  fzopredsuc  48667