Theorem unidm 4127

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

Syntax hints:   = wceq 1533   ∈ wcel 2110   ∪ cun 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3940

This theorem is referenced by:  unundi  4145  unundir  4146  uneqin  4254  difabs  4267  undifabs  4425  dfif5  4482  dfsn2  4579  unisng  4856  dfdm2  6131  unixpid  6134  fun2  6540  resasplit  6547  xpider  8367  pm54.43  9428  dmtrclfv  14377  lefld  17835  symg2bas  18520  gsumzaddlem  19040  pwssplit1  19830  plyun0  24786  wlkp1  27462  cycpmco2f1  30766  carsgsigalem  31573  sseqf  31650  probun  31677  nodenselem5  33192  filnetlem3  33728  pibt2  34697  mapfzcons  39311  diophin  39367  pwssplit4  39687  fiuneneq  39795  rclexi  39973  rtrclex  39975  dfrtrcl5  39987  dfrcl2  40017  iunrelexp0  40045  relexpiidm  40047  corclrcl  40050  relexp01min  40056  cotrcltrcl  40068  clsk1indlem3  40391  fiiuncl  41325  fzopredsuc  43522