Theorem unidm 4082

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

Syntax hints:   = wceq 1539   ∈ wcel 2108   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888

This theorem is referenced by:  unundi  4100  unundir  4101  uneqin  4209  difabs  4224  undifabs  4408  dfif5  4472  dfsn2  4571  unisng  4857  dfdm2  6173  unixpid  6176  fun2  6621  resasplit  6628  xpider  8535  pm54.43  9690  dmtrclfv  14657  lefld  18225  symg2bas  18915  gsumzaddlem  19437  pwssplit1  20236  plyun0  25263  wlkp1  27951  cycpmco2f1  31293  carsgsigalem  32182  sseqf  32259  probun  32286  nodenselem5  33818  filnetlem3  34496  pibt2  35515  metakunt21  40073  metakunt22  40074  metakunt24  40076  mapfzcons  40454  diophin  40510  pwssplit4  40830  fiuneneq  40938  rclexi  41112  rtrclex  41114  dfrtrcl5  41126  dfrcl2  41171  iunrelexp0  41199  relexpiidm  41201  corclrcl  41204  relexp01min  41210  cotrcltrcl  41222  clsk1indlem3  41542  fiiuncl  42502  fzopredsuc  44703