Theorem unidm 4117

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

Syntax hints:   = wceq 1541   ∈ wcel 2106   ∪ cun 3911

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-un 3918

This theorem is referenced by:  unundi  4135  unundir  4136  uneqin  4243  difabs  4258  undifabs  4442  dfif5  4507  dfsn2  4604  unisng  4891  dfdm2  6238  unixpid  6241  fun2  6710  resasplit  6717  xpider  8734  pm54.43  9946  dmtrclfv  14915  lefld  18495  symg2bas  19188  gsumzaddlem  19712  pwssplit1  20577  plyun0  25595  nodenselem5  27073  addsproplem6  27329  wlkp1  28692  cycpmco2f1  32043  carsgsigalem  33004  sseqf  33081  probun  33108  filnetlem3  34928  pibt2  35961  metakunt21  40670  metakunt22  40671  metakunt24  40673  mapfzcons  41097  diophin  41153  pwssplit4  41474  fiuneneq  41582  rclexi  42009  rtrclex  42011  dfrtrcl5  42023  dfrcl2  42068  iunrelexp0  42096  relexpiidm  42098  corclrcl  42101  relexp01min  42107  cotrcltrcl  42119  clsk1indlem3  42437  fiiuncl  43395  fzopredsuc  45675